add some lookup_{union,difference} lemmas
Compare changes
more things from Simuliris
lookup_union_Some_l_inv, lookup_union_Some_r_inv allow exploiting statements of the form (m1 ∪ m2) !! i = Some x.lookup_union_is_Some, lookup_difference_is_Some match the existing lookup_insert_is_Some.