exact hnil
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
Γ : SigmaPiDelta
P : M → Prop
hP : (Γ, 1)-Predicate P
hnil : P ∅
hcons : ∀ (s x : M), Seq s → P s → P (s ⁀' x)
ih : ∀ y < ∅, Seq y → P y
sseq : Seq ∅
⊢ P ∅
no goals