case refl.step.inst.refl e' e => exact absurd hp $ ne_of_ssubset e.progress_ssubset
α : Type
inst✝ : Proper α
s s₁ s₂ e' : State α
n : State.Nontrivial e'
ht : e'.tag = s₂.tag
hp : e'.progress = s₂.progress
e : e' ↓ᵢ| s₂
⊢ e' = s₂
no goals