rcases this with (rfl | ⟨x, s, Hs', rfl⟩)
case mpr.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
s : M
Hs : Seq s
hsk : lh s = k + 1
hs : ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
this : s = ∅ ∨ ∃ x s', Seq s' ∧ s = s' ⁀' x
⊢ s ∈ a ^ˢ k ×ˢ a
case mpr.intro.intro.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
Hs : Seq ∅
hsk : lh ∅ = k + 1
hs : ∀ (i z : M), ⟪i, z⟫ ∈ ∅ → z ∈ a
⊢ ∅ ∈ a ^ˢ k ×ˢ a

case mpr.intro.intro.inr.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a k : M
ih : ∀ {s : M}, s ∈ a ^ˢ k ↔ Seq s ∧ lh s = k ∧ ∀ (i z : M), ⟪i, z⟫ ∈ s → z ∈ a
x s : M
Hs' : Seq s
Hs : Seq (s ⁀' x)
hsk : lh (s ⁀' x) = k + 1
hs : ∀ (i z : M), ⟪i, z⟫ ∈ s ⁀' x → z ∈ a
⊢ s ⁀' x ∈ a ^ˢ k ×ˢ a