Imp: Adds proof of ceval_example2