case refl.step.inst.step.inst e _ f' f => exact e.nonrepeatable f |>.elim
α : 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
s₂✝¹ : State α
e : s✝ ↓ᵢ| s₂✝¹
s₂✝ : State α
f' : Steps s₂✝ tl₂
f : s₂✝¹ ↓ᵢ| s₂✝
⊢ s₁ = s₂
no goals