cases is <;> cases cs <;> simp
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 = []
no goals