exact absurd rfl (hp.right ▸ e'.rcns_ne_nil)
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝¹ : State α
e : s₁✝ ↓ᵢ s₂✝¹
s₂✝ : State α
a✝ : s₁✝ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₂
hp : rcn e = rcn a✝ ∧ [] = rcns e'
⊢ s₂✝¹.rtr = s₂.rtr ∧ s₂✝¹.events = s₂.events
no goals