Solution for Repr.triple_cps_facto_aux
intros n. induction_wf IH: (downto 0) n.
xwp. xapp. xif; intros Hn.
{ xapp. xsimpl. rewrite facto_init; math. }
{ xfun. intros f Hf. xapp. xapp (>> IH (fun a => F (n*a))).
{ math. }
{ math. }
{ intros. xapp. xapp. xapp. xsimpl*. }
{ xsimpl. rewrite (@facto_step n); math. } }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
