more view-shifts), stated lemmas about hoare triples.

definitions pushed through, some lemmas commented out for now.

(open, close, transitive, false), stated some other.

carrier of the monoid. This now corresponds exactly to the formulation
of monoids in rose.v

and the subsequent problem with instance preference in RecDom.PCM.

laters are now proved (*not* the lemmas about later commuting with stuff).