have ⟨hd, tl, h⟩ := e₂.rcns_cons
α : 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 : rcn e₁ :: rcns e₁' ~ rcns e₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
a✝ : s ↓ᵢ s₂
he₂ : rcn a✝ = rcn e₁ ∧ [] = List.erase (rcns e₂) (rcn e₁)
⊢ False
α : 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 : rcn e₁ :: rcns e₁' ~ rcns e₂
hm : rcn e₁ ∈ rcns e₂
hm' : rcns e₂ ≮[s.rtr] rcn e₁
a✝ : s ↓ᵢ s₂
he₂ : rcn a✝ = rcn e₁ ∧ [] = List.erase (rcns e₂) (rcn e₁)
hd : ID
tl : List ID
h : rcns e₂ = hd :: tl
⊢ False