case single e =>
  cases e₂ <;> simp [rcns] at hp ⊢
  case single e' => simp [e.deterministic e' hp]
  case trans e'  => exact absurd rfl (hp.right ▸ e'.rcns_ne_nil)
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ : State α
e : s₁✝ ↓ᵢ s₂✝
e₂ : s₁✝ ↓ᵢ+ s₂
hp : rcns (single e) ~ rcns e₂
⊢ s₂✝.rtr = s₂.rtr ∧ s₂✝.events = s₂.events
no goals