proposition: Lemma apps_aeq_r : forall n (vs : Tes n) v t, t ~~ apps v vs -> exists u us, t = apps u us /\ u ~~ v /\ vaeq us vs.
proof: Proof. induction vs; simpl; intros v t a. ex t (@Vnil Te). simpl. intuition. rename h into w. destruct (IHvs _ _ a) as [u [us [h1 [h2 h3]]]]. inv_aeq_0 h2; clear h2; subst. ex u0 (Vcons u1 us). simpl. rewrite Vforall2_cons_eq. intuition. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)