Solution for Wand.Hor.HorExample.MList_using_hor
intros. applys himpl_antisym.
{ destruct L as [|x L'].
{ rewrite MList_nil. applys himpl_hor_r_l_trans. xsimpl*. }
{ rewrite MList_cons. xpull. intros q.
applys himpl_hor_r_r_trans. xsimpl*. } }
{ applys himpl_hor_l.
{ xpull. intros (->&->). rewrite MList_nil. xsimpl*. }
{ xpull. intros x q L' ->. rewrite MList_cons. xsimpl*. } }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
