all_goals cases ‹Steps _ _›
case refl.step.inst
α : 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✝¹ : Steps s₂✝ s₂
a✝ : s✝ ↓ᵢ| 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 refl.step.inst.refl
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
ht : s✝.tag = s₂.tag
hp : s✝.progress = s₂.progress
a✝ : s✝ ↓ᵢ| s₂
⊢ s✝ = s₂

case refl.step.inst.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✝² : s✝ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Step s₂✝¹ s₂✝
a✝ : Steps s₂✝ s₂
⊢ s✝ = s₂

case step.refl.inst.refl
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝ : State α
n : State.Nontrivial s₂
a✝ : 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
⊢ s₂✝ = s₂

case step.refl.inst.step
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝¹ s₃✝ : State α
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₂✝ : State α
a✝¹ : Step s₂✝¹ s₂✝
a✝ : Steps s₂✝ s₃✝
⊢ s₃✝ = s₂