case trans s₁ s₂ s₄ e' e'' hi =>
  cases hm
  case inl hm =>
    simp [hm] at hr
    have ⟨_, f, f', ⟨hf₁, hf₂⟩⟩ := e.prepend_indep e' hr.cons_head
    exists trans f $ trans f' e''
    simp [hm, rcns, ←hf₁, ←hf₂]
  case inr hm =>
    have ⟨f, hf⟩ :=  hi e' hm $ hr.cons_tail.equiv e.equiv
    cases f <;> simp [rcns] at hf
    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 = rcn e' ∨ i ∈ rcns e''
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
no goals