Theorem: Execution.Step.Apply.preserves_progress (ReactorModel/Execution/Theorems/Step/Apply.lean)

State before:
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂ s₂' s₁₂ s₂₁ : State α
c : Change
e : s₁ -[c]→ s₂
⊢ s₁.progress = s₂.progress
Tactic:
cases e <;> simp [schedule_preserves_progress]
State after:
no goals