Solution for Repr.SizedStack.triple_pop
introv N. xwp. unfold Stack. xpull. intros p.
destruct L as [|x L']; tryfalse.
xapp. xchange (MList_cons p). intros q.
xapp. xapp. xapp. xapp. xapp. xapp. xapp. xval. xsimpl*.
rew_list. math.
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback