almost finish exp_to_Cexp_correct

one cheat remaining about do_Ceq (the equality case)