The general idea is to first import/export modules which are further
than the current one, and then import/export modules which are close
dependencies.

This commit tries to use the same order of imports for every file, and
describes the convention in ProofGuide.md. There is one exception,
where we do not follow said convention: in program_logic/weakestpre.v,
using that order would break printing of texan triples (??).

This commit closes issue #265.

We have these instances for all other logical operations too to support
setoid rewriting in both directions.

Simon knows why ;)

Turn all `f_op` lemmas to have shape `f (x ⋅ y) = f x ⋅ f y`, following the plan
in !295 (comment 39151), plus
`cmra_morphism_op`.

Based on @Blaisorblade's suggestion.

- And use prop_ext instead of prop_ext_2 in other proofs.

And shorten the proof.

A more general implication from `head_reducible` to `reducible`.