cases tail₁.closed_to_none e.closed
α : 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₂
e : 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 refl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
n : State.Nontrivial tl₂
e : 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₂