have : s = ∅ ∨ ∃ x s', Seq s' ∧ s = s' ⁀' x := sseq.cases
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)
s : M
ih : ∀ y < s, Seq y → P y
sseq : Seq s
⊢ P s
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)
s : M
ih : ∀ y < s, Seq y → P y
sseq : Seq s
this : s = ∅ ∨ ∃ x s', Seq s' ∧ s = s' ⁀' x
⊢ P s