case refl.trans e e'   => 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 α
ht : s✝.tag = s₂.tag
s₂✝ : State α
e : s✝ ↓ₜ s₂✝
e' : RTC s₂✝ s₂
⊢ s✝ = s₂
no goals