have h' := e'.rcns.erase_cons_tail <| by simp only [beq_iff_eq]; exact head_not_mem_tail e e' h
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
e : s₁ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₂
hr : rcn e :: rcns e' ≮[s₁.rtr] i
h : i ∈ rcns e'
⊢ ∃ e'_1, rcns e'_1 = i :: List.erase (rcn e :: rcns e') i
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
e : s₁ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₂
hr : rcn e :: rcns e' ≮[s₁.rtr] i
h : i ∈ rcns e'
h' : List.erase (rcn e :: rcns e') i = rcn e :: List.erase (rcns e') i
⊢ ∃ e'_1, rcns e'_1 = i :: List.erase (rcn e :: rcns e') i