simpa using lt_of_lt_of_le (depth_pos w) h
case zero
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
w : WType β
h : w.depth ≤ 0
⊢ encode ⟨w, h⟩ = elim' ℕ encode 0 ⟨w, h⟩
no goals