intro z₁ hz₁ z₂ hz₂ h₁ 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
hi : i < lh s₁
⊢ ∀ z₁ < s₁, ∀ z₂ < s₂, ⟪i, z₁⟫ ∈ s₁ → ⟪i, z₂⟫ ∈ s₂ → z₁ = z₂
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
hi : i < lh s₁
z₁ : M
hz₁ : z₁ < s₁
z₂ : M
hz₂ : z₂ < s₂
h₁ : ⟪i, z₁⟫ ∈ s₁
h₂ : ⟪i, z₂⟫ ∈ s₂
⊢ z₁ = z₂