case trans s sₘ₁ s₁ e₁ e₁' hi =>
  have hm := hp.mem_iff.mp $ List.mem_cons_self _ _
  have hm' := e₁'.head_minimal e₁ |>.perm hp
  have ⟨e₂, he₂⟩ := e₂.prepend_minimal hm hm'
  cases e₂ <;> simp [rcns] at he₂
  case trans sₘ₂ e₂ e₂' =>
    have ⟨h, h'⟩ := he₂
    cases e₁.deterministic e₂ h.symm
    apply hi e₂'
    rw [h']
    exact List.perm_cons _ |>.mp (hp.trans $ List.perm_cons_erase hm)
  case single =>
    exfalso
    simp [rcns] at hp
    have ⟨hd, tl, h⟩ := e₂.rcns_cons
    have ⟨_, _, h'⟩ := e₁'.rcns_cons
    simp [h, h'] at hp he₂
    have h := he₂.right.symm ▸ List.erase_cons e₁.rcn hd tl
    split at h <;> try assumption
    simp [←h] at hp
α : Type
inst✝ : Proper α
s✝ s₁✝ s₂ s sₘ₁ s₁ : State α
e₁ : s ↓ᵢ sₘ₁
e₁' : sₘ₁ ↓ᵢ+ s₁
hi : ∀ (e₂ : sₘ₁ ↓ᵢ+ s₂), rcns e₁' ~ rcns e₂ → s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
e₂ : s ↓ᵢ+ s₂
hp : rcns (trans e₁ e₁') ~ rcns e₂
⊢ s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
no goals