exact schedule_events_congr he
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
no goals