proposition: Lemma apps_aeq_l : forall n (vs : Tes n) v t, apps v vs ~~ t -> exists u us, t = apps u us /\ u ~~ v /\ vaeq us vs.
proof: Proof. intros n vs v t e. apply apps_aeq_r. hyp. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)