simp
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
a : α
f : β a → WType β
h : (WType.mk a f).depth ≤ s + 1
⊢ encode a = encode a ∧ (encode fun b => ⟨f b, ⋯⟩) = encode fun b => encode (ofWType (f b) s ⋯)
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s : ℕ
a : α
f : β a → WType β
h : (WType.mk a f).depth ≤ s + 1
⊢ (encode fun b => ⟨f b, ⋯⟩) = encode fun b => encode (ofWType (f b) s ⋯)