more things from Simuliris
-
lookup_union_Some_l_inv,lookup_union_Some_r_invallow exploiting statements of the form(m1 ∪ m2) !! i = Some x. -
lookup_union_is_Some,lookup_difference_is_Somematch the existinglookup_insert_is_Some.
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.