proposition: Lemma clos_aeq_eq R : clos_aeq R == aeq @ (R @ aeq).
proof: Proof. split. intros t u tu. destruct (clos_aeq_inv tu) as [t' [u' [tt' [uu' t'u']]]]; clear tu. ex t'. intuition. ex u'. intuition. intros t u [t' [tt' [u' [t'u' u'u]]]]. eapply clos_aeq_intro. apply tt'. sym. apply u'u. hyp. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)