induction e₁
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : rcns e₁ ~ rcns e₂
⊢ s₁.rtr = s₂.rtr ∧ s₁.events = s₂.events
case single
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ : State α
a✝ : s₁✝ ↓ᵢ s₂✝
e₂ : s₁✝ ↓ᵢ+ s₂
hp : rcns (single a✝) ~ rcns e₂
⊢ s₂✝.rtr = s₂.rtr ∧ s₂✝.events = s₂.events

case trans
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝¹ : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
a_ih✝ : ∀ (e₂ : s₂✝ ↓ᵢ+ s₂), rcns a✝ ~ rcns e₂ → s₃✝.rtr = s₂.rtr ∧ s₃✝.events = s₂.events
e₂ : s₁✝ ↓ᵢ+ s₂
hp : rcns (trans a✝¹ a✝) ~ rcns e₂
⊢ s₃✝.rtr = s₂.rtr ∧ s₃✝.events = s₂.events