Theorem: HMem.Stack.step_eq_execution (HMem/Program/Step.lean)

State before:
s : Stack
t : Thunk
cs : List (Thunk × List Bool)
⊢ step s = execution t cs → ∃ t' cs', s = execution t' cs'
Tactic:
cases s <;> simp
State after:
no goals