How to deal with `emp`, `True`, and friends when the BI is ambigious
The following discussion from !115 (merged) should be addressed:
We often write
emp : PROP. However, since coercions are explicit term constructors in Coq, this apparently leads to unification problems here and there.
The alternative is to write
bi_emp (PROP:=PROP), which is ugly.
Maybe we should have special notations to force the type arguments of
True, and friends.
I think ssr is also doing something like that. Depending on the outcome of this issue, we should not just address the occurrence in !115 (merged), but also fix other occurrences.