proposition: Lemma incl_clos_aeq R : R << clos_aeq R.
proof: Proof. intros u v uv. apply clos_aeq_intro with (u':=u) (v':=v). refl. refl. hyp. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)