proposition: Lemma clos_mon_min R S : Monotone S -> R << S -> clos_mon R << S.
proof: Proof. intros S_mon RS. intros u v; revert u v; induction 1; mon. fo. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)