proofs. One change to axiomatisation was needed.

On branch coq-ho
Changes not staged for commit:
	modified:   coq-ho/core_lang.v
Untracked files:
	coq-ho/Makefile
no changes added to commit (use "git add" and/or "git commit -a")
On branch coq-ho
Changes not staged for commit:
	modified:   coq-ho/core_lang.v
Untracked files:
	coq-ho/Makefile
no changes added to commit (use "git add" and/or "git commit -a")

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).