simp[elimDecode, encodeDecode_eq_encode_map_decode]
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
⊢ encodeDecode (SubWType β s) e = elimDecode β (fun a l => encode (a, l)) s e
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
⊢ Option.map encode (decode e) =
    Option.map (elim' ℕ (fun x => (encode x.fst).pair (encode (List.ofFn (fintypeArrowEquivFinArrow x.snd)))) s)
      (decode e)