case refl.step.inst.refl e =>
  cases tail₂.closed_to_none e.closed
  cases tail₁
  case none   => exact absurd hp $ ne_of_ssubset e.progress_ssubset
  case some f => exact f.deterministic e.exec hp
α : 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₂
no goals