simp[encode_eq, SubWType.ofW, depth, SubWType.encode_mk]
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
a : α
f : β a → WType β
⊢ encode (mk a f) =
    ((Finset.univ.sup fun n => (f n).depth) + 1).pair ((encode a).pair (encode fun b => (encode (f b)).unpair.2))
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
a : α
f : β a → WType β
⊢ (fun b => encode (SubWType.ofWType (f b) (Finset.univ.sup fun n => (f n).depth) ⋯)) = fun b =>
    encode (SubWType.ofWType (f b) (f b).depth ⋯)