proposition: Lemma clos_mon_sym R : Symmetric R -> Symmetric (clos_mon R).
proof: Proof. intros R_sym u v; revert u v; induction 1. apply m_step. hyp. apply m_app_l. hyp. apply m_app_r. hyp. apply m_lam. hyp. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)