exact e₁₂.preserves_events ▸ e₁.preserves_events ▸ e₂₁.preserves_events ▸ e₂.preserves_events
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
⊢ s₁₂.events = s₂₁.events
no goals