exact depth_lt_depth_mk _ _ _
case mk.mk.mk.mk.mk
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁸ : Primcodable τ
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : Inhabited (WType β)
fs : τ → α × σ → σ
fγ : τ → σ × α × List γ → γ
g : τ → σ
w : τ → WType β
hfs : Primrec₂ fs
hfγ : Primrec₂ fγ
hg✝ : Primrec g
hw : Primrec w
hm : Primrec fun p => p.2.2.depth
hl : Primrec fun p => List.map (fun w => (p.1, fs p.1 (p.2.2.inversion.1, p.2.1), w)) p.2.2.inversion.2
hg : Primrec₂ fun p l => fγ p.1 (p.2.1, p.2.2.inversion.1, l)
z : τ
x : σ
a : α
f : β a → WType β
i : Fin (Fintype.card (β a))
⊢ (f (fintypeEquivFin.symm i)).depth < (WType.mk a f).depth
no goals