Theorem: Execution.Grouped.Tail.deterministic (ReactorModel/Execution/Theorems/Grouped/Tail.lean)

State before:
α : Type
inst✝ : Proper α
s s₁✝ s₂ s₁ : State α
e : s ↓ᵢ+ s₁
hp : s₁.progress = s.progress
⊢ s.progress = s₁.progress
Tactic:
simp [hp]
State after:
no goals