Solution for Repr.triple_cps_append_aux
introv Hk. gen H p1 p2 L2 k. induction_wf IH: list_sub L1.
xwp. xapp. xchange (MList_if p1). xif; intros C; case_if; xpull.
{ intros ->. xapp. xsimpl*. }
{ intros x p1' L1' ->. xapp. xfun. intros f Hf.
xapp (>> IH (H \* p1 ~~~> `{ head := x ; tail := p1' })).
{ auto. }
{ intros p3. xapp. xapp. xapp. xchanges <- MList_cons. }
{ xsimpl. } }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
