cases ‹Step _ _›
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.refl.inst
α : 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
n : State.Nontrivial s₂
a✝ : s₂ ↓ᵢ| s₂✝
⊢ s₃✝ = s₂

case step.refl.time
α : 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
n : State.Nontrivial s₂
a✝ : s₂ ↓ₜ s₂✝
⊢ s₃✝ = s₂