Solution for Repr.triple_cps_facto
xwp. xfun. intros f Hf.
xapp (>> triple_cps_facto_aux (fun (a:int) => a)).
{ auto. }
{ intros a. xapp. xval. xsimpl*. }
{ xsimpl*. }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
