all_goals cases ‹Steps _ _›
case refl.step.inst
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
s₂✝ : State α
a✝¹ : Steps s₂✝ tl₂
a✝ : s✝ ↓ᵢ| s₂✝
⊢ s₁ = s₂

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

case refl.step.inst.step
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
s₂✝¹ : State α
a✝² : s✝ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Step s₂✝¹ s₂✝
a✝ : Steps s₂✝ tl₂
⊢ s₁ = s₂

case step.refl.inst.refl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝ : State α
n : State.Nontrivial tl₂
a✝ : tl₂ ↓ᵢ| s₂✝
a_ih✝ : State.Nontrivial s₂✝ → Tail s₂✝ s₁ → Steps s₂✝ tl₂ → s₂✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₂✝ s₁
ht : s₂✝.tag = tl₂.tag
⊢ s₁ = s₂

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