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 I L A iter T₁ : M
left✝¹ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
T₂ : M
left✝ : T₂ < U
HT₂ : IsSeries U I L A iter T₂
Hₛ₂ : T₂{L}[0] = 0
i : M
⊢ i ≤ iter → T₁{L}[i] = T₂{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 I L A iter T₁ : M
left✝¹ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
T₂ : M
left✝ : T₂ < U
HT₂ : IsSeries U I L A iter T₂
Hₛ₂ : T₂{L}[0] = 0
⊢ 𝚺₀-Predicate fun i => i ≤ iter → T₁{L}[i] = T₂{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 I L A iter T₁ : M
left✝¹ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
T₂ : M
left✝ : T₂ < U
HT₂ : IsSeries U I L A iter T₂
Hₛ₂ : T₂{L}[0] = 0
⊢ 0 ≤ iter → T₁{L}[0] = T₂{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 I L A iter T₁ : M
left✝¹ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
T₂ : M
left✝ : T₂ < U
HT₂ : IsSeries U I L A iter T₂
Hₛ₂ : T₂{L}[0] = 0
x✝ : M
a✝ : x✝ ≤ iter → T₁{L}[x✝] = T₂{L}[x✝]
⊢ x✝ + 1 ≤ iter → T₁{L}[x✝ + 1] = T₂{L}[x✝ + 1]