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

State before:
m : Memory
is p : Program
cs : List (Thunk × List Bool)
r : Memory
⊢ step (execution { state := m, current := is, function := p } cs) = result r → m = r ∧ is = Program.exit ∧ cs = []
Tactic:
cases is <;> cases cs <;> simp
State after:
no goals