simp [exit_of_step_result h]
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 }
      []
no goals