Proof mode support for monotonous predicates.
Also, developed a notion of "BI embedding", which is a general notion that is useful for supporting monPred in proofmode.
Also, developed a notion of "BI embedding", which is a general notion that is useful for supporting monPred in proofmode.