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