proposition: Lemma eta_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. induction us; simpl; intros u t e. exists t. exists Vnil. split_all. apply left_sym. hyp. destruct (IHus _ _ e) as [v [vs [h1 h2]]]. inversion h2; subst. inversion H0; subst. inversion H. ex u' (Vcons h vs). split_all. apply left_sym. hyp. ex u (Vcons v' vs). split_all. apply right_sym. apply left_sym. hyp. ex u (Vcons h vs). split_all. do 2 apply right_sym. hyp. Qed.
imports: Coq(Morphisms Basics) CoLoR(LogicUtil RelUtil VecOrd VecUtil)