fact: Definition monotonous := forall T (pos: Pos T) (Mpos: PlaceHolder pos) (Npos: PlaceHolder pos), proj1_sig2 Mpos -R-> proj1_sig2 Npos -> swap Mpos -R-> swap Npos.
imports: CoLoR(RelExtras ListExtras TermsBuilding)