simp[depth, Equiv.vectorEquivFin]
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
a : α
l : List (SubWType β s)
v : Vector (SubWType β s) (Fintype.card (β a))
⊢ (WType.mk a fun b => ↑(fintypeArrowEquivVector.symm v b)).depth ≤ s + 1
no goals