case mk
α : Type u_1
β : α → Type u_2
inst✝ : (a : α) → Fintype (β a)
a✝ : α
f✝ : β a✝ → WType β
⊢ 0 < depth (mk a✝ f✝)
α : Type u_1
β : α → Type u_2
inst✝ : (a : α) → Fintype (β a)
t : WType β
⊢ 0 < depth t
cases t
no goals
case mk
α : Type u_1
β : α → Type u_2
inst✝ : (a : α) → Fintype (β a)
a✝ : α
f✝ : β a✝ → WType β
⊢ 0 < depth (mk a✝ f✝)
apply Nat.succ_pos