add some lookup_{union,difference} lemmas
All threads resolved!
All threads resolved!
Compare changes
+ 24
− 7
@@ -2043,13 +2043,6 @@ Proof. rewrite lookup_union. destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
@@ -2062,6 +2055,19 @@ Proof. intro. rewrite lookup_union_Some_raw; intuition. Qed.
@@ -2069,6 +2075,14 @@ Proof.
@@ -2525,6 +2539,9 @@ Proof.