Also:

- Remove the wp_strip_later hack.
- Let wp_lam, wp_rec, wp_... initiate the proof mode.

Really, *all* of our files contain proof rules

Thanks to Robbert for fixing gen_heap

Use COFEs only for the recursive domain equation solver

This way we avoid the env_cbv tactic unfolding string related stuff
that appears in the goal and hypotheses of the proof mode.

And also rename the corresponding proof mode tactics.

rename program_logic.{ownership -> wsat}. It really is about world satisfaction and invariants more than about ownership.

Used in iRevert, iClear, iFrame, and for generalizing the IH in
iInduction and iLöb.

This makes stuff more uniform and also removes the need for the [inGFs]
type class. Instead, there is now a type class [subG Σ1 Σ2] which expresses
that a list of functors [Σ1] is contained in [Σ2].