case succ i IH =>
  intro hi
  have h₁ : S₁{L}[i + 1] = S₁{L}[i] + fbit A (start + i) := HS₁ i (lt_iff_succ_le.mpr hi)
  have h₂ : S₂{L}[i + 1] = S₂{L}[i] + fbit A (start + i) := HS₂ i (lt_iff_succ_le.mpr hi)
  simp [IH (le_trans (by simp) hi), h₁, h₂]
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U L A start intv S₁ : M
left✝¹ : S₁ < U
HS₁ : IsSegment L A start intv S₁
S₂ : M
left✝ : S₂ < U
HS₂ : IsSegment L A start intv S₂
Hₛ : S₁{L}[0] = S₂{L}[0]
i : M
IH : i ≤ intv → S₁{L}[i] = S₂{L}[i]
⊢ i + 1 ≤ intv → S₁{L}[i + 1] = S₂{L}[i + 1]
no goals