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)
α : 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₂✝
hm : rcn e₁ ∈ rcns e₂✝
hm' : rcns e₂✝ ≮[s.rtr] rcn e₁
sₘ₂ : State α
e₂ : s ↓ᵢ sₘ₂
e₂' : sₘ₂ ↓ᵢ+ s₂
he₂ : rcn e₂ = rcn e₁ ∧ rcns e₂' = List.erase (rcns e₂✝) (rcn e₁)
⊢ s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
no goals