that performs `wp_pure` in small steps until the lemma matches the goal.

add some big_opS lemmas

See merge request !619

strengthen cmra_op_discrete

See merge request !618

add Cinl_valid, Cinr_valid

See merge request !621

reuse PreG class in G class where possible

See merge request !617

gen_heap: expose that inG identities are preserved

See merge request !585

Done with a script by Tej; see
iris/iris!609 for details.

Better errors when opening an invariant/mask changing update around a non-atomic WP

See merge request !614

This makes sure that when trying to open an invariant or to eliminate a mask-changing
update around a non-atomic WP that it doesn't fail with "cannot eliminate modality",
but instead gives an side-condition `Atomic ...` informing the user what's going on.

Unlike the class `ElimModal` and `ElimInv`, the class `ElimAcc` was not yet equipped
with a Coq side-condition. This commit adds such a side-condition.