Commit ef59f1b0 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix for recent std++.

parent 7f2f81e1
......@@ -185,7 +185,7 @@ Section map.
iApply ("HΦ" $! (ys' ++ map x)). iSplit.
+ iPureIntro. rewrite (gmultiset_disj_union_difference {[ x ]} X)
-?gmultiset_elem_of_singleton_subseteq //.
rewrite (comm disj_union) gmultiset_elements_disj_union.
rewrite (comm_L disj_union) gmultiset_elements_disj_union.
by rewrite gmultiset_elements_singleton assoc_L bind_app -Hys /= right_id_L.
+ by rewrite -assoc_L.
Qed.
......
......@@ -160,7 +160,7 @@ Section mapper.
rewrite -assoc_L. iApply ("HΦ" $! (map x ++ ys') with "[$Hcsort]").
iPureIntro. rewrite (gmultiset_disj_union_difference {[ x ]} X)
-?gmultiset_elem_of_singleton_subseteq //.
rewrite (comm disj_union) gmultiset_elements_disj_union.
rewrite (comm_L disj_union) gmultiset_elements_disj_union.
by rewrite gmultiset_elements_singleton assoc_L bind_app -Hys /= right_id_L comm.
Qed.
......@@ -266,7 +266,7 @@ Section mapper.
iApply ("HΦ" $! (zs' ++ red i ys)). iSplit; last by rewrite -assoc_L.
iPureIntro. rewrite (gmultiset_disj_union_difference {[ i,ys ]} Y)
-?gmultiset_elem_of_singleton_subseteq //.
rewrite (comm disj_union) gmultiset_elements_disj_union.
rewrite (comm_L disj_union) gmultiset_elements_disj_union.
rewrite gmultiset_elements_singleton assoc_L Hzs !bind_app /=.
by rewrite right_id_L !assoc_L.
Qed.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment