case trans f f'' =>
  have ⟨h₁, h₂⟩ := hf
  have ⟨_, f, f', ⟨hf₁, hf₂⟩⟩ := e.prepend_indep f $ h₁.symm ▸ hr |>.cons_head
  exists trans f $ trans f' f''
  have h₃ := e''.rcns.erase_cons_tail <| by
    simp only [beq_iff_eq]; exact head_not_mem_tail e' e'' hm
  simp [rcns, hf₁, h₁, hf₂, h₂, h₃]
α : 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₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
s₂✝ : State α
f : s₁✝ ↓ᵢ s₂✝
f'' : s₂✝ ↓ᵢ+ s₄
hf : rcn f = i ∧ rcns f'' = rcn e' :: List.erase (rcns e'') i
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
no goals