Theorem: Execution.Instantaneous.Closed.progress_eq (ReactorModel/Execution/Theorems/Grouped/Instantaneous.lean)

State before:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
e₁ : s ↓ᵢ| s₁
e₂ : s ↓ᵢ| s₂
⊢ s₁.progress = s₂.progress
Tactic:
simp [e₁.progress_def, e₂.progress_def]
State after:
no goals