Solution for Repr.triple_cps_append
xwp. xfun. intros f Hf.
set (Q := funloc p3 => MList (L1++L2) p3).
xapp (@triple_cps_append_aux \[] Q).
{ intros p3. xapp. xval. unfold Q. xsimpl*. }
{ xsimpl. }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
