{ simp[SubWType.encode_eq_elim']; apply SubWType.elim_const; simp }
case some
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
e : ℕ
w : SubWType β e.unpair.1
⊢ encode (SubWType.ofWType (↑w) (↑w).depth ⋯) = encode w
no goals