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.

(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