Theorem: HMem.Stack.exit_of_step_result' (HMem/Program/Step.lean)

State before:
cs : List (Thunk × List Bool)
r state✝ : Memory
current✝ function✝ : Program
h : step (execution { state := state✝, current := current✝, function := function✝ } cs) = result r
⊢ execution { state := state✝, current := current✝, function := function✝ } cs =
    execution
      { state := r, current := Program.exit,
        function := { state := state✝, current := current✝, function := function✝ }.function }
      []
Tactic:
simp [exit_of_step_result h]
State after:
no goals