Solution for Repr.triple_mfree
intros. gen p. induction_wf IH: list_sub L. intros.
xwp. xapp. xchange MList_if. xif; intros C; case_if; xpull.
{ intros x p' L' ->. xapp. xapp. xapp. xsimpl. }
{ intros ->. xval. xsimpl. }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
