have ⟨_, f, f', ⟨hf₁, hf₂⟩⟩ := e.prepend_indep e' hr.cons_head
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hm : i = rcn e'
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] rcn e'
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hm : i = rcn e'
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] rcn e'
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂
hf₁ : rcn f = rcn e'
hf₂ : rcn f' = rcn e
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i