case single e' =>
  have ⟨_, f, f', ⟨hf₁, hf₂⟩⟩ := e.prepend_indep e' $ hm ▸ hr.cons_head
  exists trans f (single f')
  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'
⊢ ∃ f, rcns f = i :: rcn e :: List.erase [rcn e'] i
no goals