exact absurd ht $ ne_of_lt $ lt_of_lt_of_le e.tag_lt e'.tag_le
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
ht : s✝.tag = s₂.tag
hp : s✝.progress = s₂.progress
s₂✝ : State α
e' : Steps s₂✝ s₂
e : s✝ ↓ₜ s₂✝
⊢ s✝ = s₂
no goals