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.
Edited by Jacques-Henri Jourdan
Also, developed a notion of "BI embedding", which is a general notion that is useful for supporting monPred in proofmode.