more things from Simuliris
lookup_union_Some_l_inv
lookup_union_Some_r_inv
(m1 ∪ m2) !! i = Some x
lookup_union_is_Some
lookup_difference_is_Some
lookup_insert_is_Some