Make `wp_apply` perform `wp_pure` in small steps until the lemma matches the goal.

See merge request !587

Rename `ofeT`→`ofe`, `cmraT`→`cmra`, and `ucmraT`→`ucmra`.

See merge request iris/iris!623

add mono_nat_auth_lb

See merge request iris/iris!605

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

add some big_opS lemmas

See merge request iris/iris!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 iris/iris!585