induction i using induction_iSigmaZero
case intro.intro.intro.intro.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 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
⊢ i ≤ intv → S₁{L}[i] = S₂{L}[i]
case intro.intro.intro.intro.intro.intro.intro.intro.hP
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]
⊢ 𝚺₀-Predicate fun i => i ≤ intv → S₁{L}[i] = S₂{L}[i]

case intro.intro.intro.intro.intro.intro.intro.intro.zero
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]
⊢ 0 ≤ intv → S₁{L}[0] = S₂{L}[0]

case intro.intro.intro.intro.intro.intro.intro.intro.succ
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]
x✝ : M
a✝ : x✝ ≤ intv → S₁{L}[x✝] = S₂{L}[x✝]
⊢ x✝ + 1 ≤ intv → S₁{L}[x✝ + 1] = S₂{L}[x✝ + 1]