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 emp
, 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.