proposition: Lemma clos_aeq_intro_refl (R : rel Te) t u : R t u -> clos_aeq R t u.
proof: Proof. intro tu. eapply clos_aeq_intro. refl. refl. hyp. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)