simp [hm, rcns, ←hf₁, ←hf₂]
α : Type
inst✝ : Proper α
s s₂ s₃ : State α
i : ID
s₁✝ s₂✝ : State α
e' : s₁✝ ↓ᵢ s₂✝
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : [rcn e, rcn e'] ≮[s₁.rtr] i
hm : i = rcn e'
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂✝
hf₁ : rcn f = rcn e'
hf₂ : rcn f' = rcn e
⊢ rcns (trans f (single f')) = i :: rcn e :: List.erase [rcn e'] i
no goals