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

State before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
c : Change
e₁ : s -[c]→ s₁
e₂ : s -[c]→ s₂
⊢ s₁ = s₂
Tactic:
cases e₁ <;> cases e₂ <;> simp <;> exact LawfulUpdate.unique ‹_› ‹_›
State after:
no goals