have ⟨_, _⟩ := rcns_perm_deterministic e₁ e₂ $ progress_eq_rcns_perm e₁ e₂ hp
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
this : s₁.tag = s₂.tag
⊢ s₁ = s₂
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
this : s₁.tag = s₂.tag
left✝ : s₁.rtr = s₂.rtr
right✝ : s₁.events = s₂.events
⊢ s₁ = s₂