proposition: Lemma clos_aeq_trans_inv : forall t u, S* t u -> t ~~ u \/ exists v, S t v /\ S* v u.
proof: Proof. induction 1. firstorder auto with crelations. fo. destruct IHclos_aeq_trans1 as [h|[t [h1 h2]]]. destruct IHclos_aeq_trans2 as [i|[t' [i1 i2]]]. left. trans v; hyp. right. ex t'. rewrite h. auto. right. ex t. split. hyp. trans v; hyp. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)