fact: Definition absMonCond := forall N N' (Nabs: isAbs N) (N'abs: isAbs N'), algebraic (absBody Nabs) -> algebraic (absBody N'abs) -> absType Nabs = absType N'abs -> absBody Nabs -R-> absBody N'abs -> N -R-> N'.
imports: CoLoR(RelExtras ListExtras TermsEta LogicUtil) Coq(Morphisms)