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 s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
e : s✝ ↓ᵢ| tl₂
⊢ s₁ = s₂
case refl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
tail₂ : Tail s₂ s₂
ht : s✝.tag = s₂.tag
e : s✝ ↓ᵢ| s₂
⊢ s₁ = s₂