proposition: Lemma eta_aeq_apps : forall n (us : Tes n) u t, apps u us =>e t -> exists v vs, t = apps v vs /\ Vcons u us ==>e Vcons v vs.
proof: Proof. intros n us u t e. inversion e; subst. destruct (apps_aeq_l H) as [v [vs [h1 [h2 h3]]]]; subst. destruct (eta_apps H1) as [w [ws [i1 i2]]]; subst. destruct (apps_aeq_r H0) as [c [cs [j1 [j2 j3]]]]; subst. ex c cs. split_all. symmetry in h2, h3, j2, j3. ex (Vcons v vs). split. fo. ex (Vcons w ws). split_all. fo. Qed.
imports: Coq(Morphisms Basics) CoLoR(LogicUtil RelUtil VecOrd VecUtil)