fixed broken proof, was missing init_Cenv
slow progress