finish proving exp_to_Cexp_correct