Add missing commutations for `fupd`

See merge request iris/iris!688

Suggestion from Gregory Malecha, forall lemmas suggested by Robbert & Ralf,
proof scripts from me.

Change the tactic for resolving Equiv and Dist from an Ofe definition.

See merge request iris/iris!689

Example include Equiv, Dist, Op, Core, Valid, ValidN and Unit.

The previous hints used eapply. The new hint now use refine. These two
tactic use a different unification algorithm, which result in
different behavior with respect to canonical structures.

The refine tactic is followed by shelving all the remaining goals,
which correspond actually to existential variables.

In particular, in RustHornBelt, the version using apply is unable to
find the canonical structure of heterogeneous lists.

Rename `big_sep{L,L2,M,M2,S}_intuitionistically_forall` and `big_orL_lookup` to `big_*_intro`

See merge request iris/iris!694

Add a `Proper` instance for ccompose.

See merge request iris/iris!695

Add `big_sepM2_union_inv_*`.

See merge request iris/iris!690

also add `wand_entails'`, which was used in some earlier version of these proofs

Thank you, Robbert.

Nested big-op lemmas

See merge request iris/iris!673

FromPure instances for big_sepM

See merge request iris/iris!626

better error when iMod/iModIntro fails due to mask mismatch

See merge request iris/iris!691

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

See merge request iris/iris!692