Theorem: Execution.State.schedule_events_congr (ReactorModel/Execution/Theorems/State.lean)

State before:
α : Type
inst✝ : Hierarchical α
s s₁✝ s₂✝ s₁ s₂ : State α
i : ID
t : Time
v : Value
h : s₁.events = s₂.events
⊢ (schedule s₁ i t v).events = (schedule s₂ i t v).events
Tactic:
simp [schedule, h]
State after:
no goals