BI are an extension of "bounded"
Conflicts: coq-ho/lib/ModuRes/Finmap.v
Conflicts: coq-ho/lib/ModuRes/BI.v
This means that bundled types are *not* visible to the Iris logic itself!
show that products preserve pcmType of the RA order, and that pcmType is trivial for discrete metrics
