add some lookup_{union,difference} lemmas

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.