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.

mentioned in issue simuliris#12

added 1 commit

• 629eac17 - shorter proof

Compare with previous version

added 1 commit

• 72fe4c78 - make names more consistent

Compare with previous version

resolved all threads

resolved all threads

resolved all threads

resolved all threads

added 14 commits

• 72fe4c78...a83b4604 - 10 commits from branch master
• 1883089d - add some lookup_{union,difference} lemmas
• 0b6efe0d - shorter proof
• 5fbf3d13 - make names more consistent
• 985e9cbd - changelog

Compare with previous version

added 5 commits

• 653c819a - 1 commit from branch master
• 1ef1316d - add some lookup_{union,difference} lemmas
• 67b0c30c - shorter proof
• a4a6317b - make names more consistent
• c288716d - changelog

Compare with previous version

Seems like I forgot to say LGTM :).

added 8 commits

• c288716d...28ed75d0 - 4 commits from branch master
• 60f310e6 - add some lookup_{union,difference} lemmas
• 3983fa93 - shorter proof
• 53e4f0f7 - make names more consistent
• 90b61523 - changelog

Compare with previous version

enabled an automatic merge when the pipeline for 90b61523 succeeds

mentioned in commit 6688588a

merged