cases e <;> cases e' <;> simp [he]
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂ s₂' s₁₂ s₂₁ : State α
c : Change
e : s₁ -[c]→ s₂
e' : s₁' -[c]→ s₂'
he : s₁.events = s₁'.events
⊢ s₂.events = s₂'.events
case act.act
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₁₂ s₂₁ : State α
he : s₁.events = s₁'.events
i✝ : ID
t✝ : _root_.Time
v✝ : Value
⊢ (schedule s₁ i✝ t✝ v✝).events = (schedule s₁' i✝ t✝ v✝).events