proof: exec (comp e) s = [eval e] = eval e : s
comp' :: Expr -> [Op]
proof: exec (comp' e c) s = exec c (eval e:s)