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 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
.