proposition: Lemma clos_mon_refl R : Reflexive R -> Reflexive (clos_mon R).
proof: Proof. intros R_refl u. apply m_step. refl. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)