induction e₁ <;> cases e₂
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e₁ : Steps s s₁
e₂ : Steps s s₂
n : State.Nontrivial s
ht : s₁.tag = s₂.tag
hp : s₁.progress = s₂.progress
⊢ s₁ = s₂
case refl.refl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
n : State.Nontrivial s₂
ht : s₂.tag = s₂.tag
hp : s₂.progress = s₂.progress
⊢ s₂ = s₂

case refl.step
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
ht : s✝.tag = s₂.tag
hp : s✝.progress = s₂.progress
s₂✝ : State α
a✝¹ : Step s✝ s₂✝
a✝ : Steps s₂✝ s₂
⊢ s✝ = s₂

case step.refl
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝ s₃✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a_ih✝ : Steps s₂✝ s₂ → State.Nontrivial s₂✝ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
a✝ : Step s₂ s₂✝
n : State.Nontrivial s₂
⊢ s₃✝ = s₂

case step.step
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝¹ s₃✝ : State α
a✝³ : Step s₁✝ s₂✝¹
a✝² : Steps s₂✝¹ s₃✝
a_ih✝ : Steps s₂✝¹ s₂ → State.Nontrivial s₂✝¹ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
n : State.Nontrivial s₁✝
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
s₂✝ : State α
a✝¹ : Step s₁✝ s₂✝
a✝ : Steps s₂✝ s₂
⊢ s₃✝ = s₂