Explicit vdash

This came as a result of the discussion in #270 (closed). It does a few things (unfortunately).

• A new prefix |- P and |-@{PROP} P that ensures that P is parsed in I scope and acts like bi_emp_valid and sbi_emp_valid.
• Removes the coercion status of bi_emp_valid and sbi_emp_valid
• It moves notations that parse to types into type_scope since that scope is already set up appropriately.
• It makes the -* at type_scope a parsing only notation.

People can decide what portions of this are good for merging.