Add lemmas `big_sepM2_inv_{l,r}` and rename `big_sepM2_lookup_{1,2}` into `big_sepM2_lookup_{l,r}`.

Merged Robbert Krebbers requested to merge robbert/big_sepM2_lookup into master

In !690 (merged) I noticed two things:

  • The proof in !690 (merged) can be simplified using the new lemmas big_sepM2_inv_{l,r}, which generalize big_sepM2_lookup_{1,2}
  • The lemmas big_sepM2_lookup_{1,2} are inconsistently named. For other lemmas, we use _l and _r, so I renamed them into big_sepM2_lookup_{l,r}.

Merge request reports