proposition: Lemma clos_aeq_inv R t u : clos_aeq R t u -> exists t' u', t ~~ t' /\ u ~~ u' /\ R t' u'.
proof: Proof. intro tu. inversion tu; clear tu; subst. ex u' v'. intuition. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)