Theorem: Execution.Step.Exec.progress_eq (ReactorModel/Execution/Theorems/Step/Exec.lean)

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
⊢ s₂.progress = Set.insert (rcn e) s₁.progress
Tactic:
simp [e.dst_eq, State.record_progress_eq, e.apply.preserves_progress]
State after:
no goals