replace h : _ ≮[_]≯ _ := { not_eq := e₁.seq_rcn_ne e₂, left := h, right := e₁.seq_wellordered e₂ }
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ᵢ s₂
e₂ : s₂ ↓ᵢ s₃
h : rcn e₁ ≮[s₁.rtr] rcn e₂
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn e₂ ∧ rcn e₂' = rcn e₁ ∧ s₃' = s₃
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ᵢ s₂
e₂ : s₂ ↓ᵢ s₃
h : rcn e₁ ≮[s₁.rtr]≯ rcn e₂
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn e₂ ∧ rcn e₂' = rcn e₁ ∧ s₃' = s₃