proposition: Lemma clos_mon_aeq_incl R : clos_mon (clos_aeq R) << clos_aeq (clos_mon R).
proof: Proof. apply clos_mon_min. apply clos_aeq_mon. apply monotone_clos_mon. apply clos_aeq_incl. intros u v uv. apply m_step. hyp. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)