rw[←encode_finArrow, encode_fintypeArrow (β a)]
case succ.mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
ih : ∀ (w : SubWType β s), encode w = elim' ℕ encode s w
this : Primcodable { t // t.depth ≤ s } := Primcodable.SubWType s
a : α
f : β a → WType β
hw : (WType.mk a f).depth ≤ s + 1
⊢ encode (List.ofFn (encode ∘ fintypeArrowEquivFinArrow fun b => ⟨f b, ⋯⟩)) = encode fun b => elim ℕ encode (f b)
case succ.mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
ih : ∀ (w : SubWType β s), encode w = elim' ℕ encode s w
this : Primcodable { t // t.depth ≤ s } := Primcodable.SubWType s
a : α
f : β a → WType β
hw : (WType.mk a f).depth ≤ s + 1
⊢ encode (encode ∘ fintypeArrowEquivFinArrow fun b => ⟨f b, ⋯⟩) =
    encode (fintypeArrowEquivFinArrow fun b => elim ℕ encode (f b))