exists single e
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
e : s₁ ↓ᵢ s₂
hr : [rcn e] ≮[s₁.rtr] i
hm : i = rcn e
⊢ ∃ e', rcns e' = i :: List.erase [rcn e] i
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
e : s₁ ↓ᵢ s₂
hr : [rcn e] ≮[s₁.rtr] i
hm : i = rcn e
⊢ rcns (single e) = i :: List.erase [rcn e] i