exact lt_of_lt_of_le hi h₁₂
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
p : Formulae k
c : Construction M p
v : Fin k → M
s : M
h : c.CSeq v s
s₁ s₂ : M
H₁ : c.CSeq v s₁
H₂ : c.CSeq v s₂
h₁₂ : lh s₁ ≤ lh s₂
i : M
ih : i < lh s₁ → ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
hi : i + 1 < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪i + 1, z₁⟫ ∈ s₁
h₂ : ⟪i + 1, z₂⟫ ∈ s₂
hi' : i < lh s₁
z' : M := ⋯.nth hi'
ih₁ : ⟪i, z'⟫ ∈ s₁
ih₂ : ⟪i, z'⟫ ∈ s₂
h₁' : ⟪i + 1, c.succ v i z'⟫ ∈ s₁
⊢ i + 1 < lh s₂
no goals