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