case succ i ih =>
  have hi' : i < lh s₁ := lt_of_le_of_lt (by simp) hi
  let z' := H₁.seq.nth hi'
  have ih₁ : ⟪i, z'⟫ ∈ s₁ := H₁.seq.nth_mem hi'
  have ih₂ : ⟪i, z'⟫ ∈ s₂ := by
    have : z' = H₂.seq.nth (lt_of_lt_of_le hi' h₁₂) :=
      ih hi' z' (by simp [z']) (H₂.seq.nth (lt_of_lt_of_le hi' h₁₂)) (by simp [z']) (by simp [z']) (by simp)
    simp [this]
  have h₁' : ⟪i + 1, c.succ v i z'⟫ ∈ s₁ := H₁.succ i (by simp [lt_tsub_iff_right, hi]) z' ih₁
  have h₂' : ⟪i + 1, c.succ v i z'⟫ ∈ s₂ := H₂.succ i (by simp [lt_tsub_iff_right]; exact lt_of_lt_of_le hi h₁₂) z' ih₂
  have e₁ : z₁ = c.succ v i z' := H₁.seq.isMapping.uniq h₁ h₁'
  have e₂ : z₂ = c.succ v i z' := H₂.seq.isMapping.uniq h₂ h₂'
  simp [e₁, e₂]
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₂
⊢ z₁ = z₂
no goals