rcases H₁ with ⟨S₁, _, HS₁, Hₛ, rfl⟩
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 nₛ nₑ₁ nₑ₂ : M
H₁ : Segment U L A start intv nₛ nₑ₁
H₂ : Segment U L A start intv nₛ nₑ₂
⊢ nₑ₁ = nₑ₂
case intro.intro.intro.intro
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 nₛ nₑ₂ : M
H₂ : Segment U L A start intv nₛ nₑ₂
S₁ : M
left✝ : S₁ < U
HS₁ : IsSegment L A start intv S₁
Hₛ : S₁{L}[0] = nₛ
⊢ S₁{L}[intv] = nₑ₂