avoid being a delta-reduction away from Setoid's equiv (WARNING: some stuff doesn't compile anymore)

Moved connective notation to BI.

Added ⁺T for ra_pos T and eliminated BI.pres since I'd rather see ⁺res than BI.pres.

Bound mask_scope to type mask.

This gets rid of an unnecessary proof obligation for wpF.

(I've seen ↓a before for validity, …)

introduce notation to provide "pres" existential witnesses by giving the missing proof. (This is a natural candidate for more ltac magic, to solve these obligations automatically... actually, why can't eauto do that?)

add first version of RA (resource algebra): validity is a decidable predicate, rather than hard-coded into the type structure

improve n[] notation for nonexpansive maps: the proof of Proper is no longer required, it can be derived from nonexpansiveness

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

definitions pushed through, some lemmas commented out for now.

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.