have : ∃ y, ⟪π₁ u, y⟫ ∈ s₁ := H₁.exists this
case h.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hl : lh s₁ = lh s₂
h : s₁ ⊆ s₂
u : M
hu : u ∈ s₂
this : π₁ u < lh s₁
⊢ u ∈ s₁
case h.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s₁ s₂ : M
H₁ : Seq s₁
H₂ : Seq s₂
hl : lh s₁ = lh s₂
h : s₁ ⊆ s₂
u : M
hu : u ∈ s₂
this✝ : π₁ u < lh s₁
this : ∃ y, ⟪π₁ u, y⟫ ∈ s₁
⊢ u ∈ s₁