proposition: Lemma beta_aeq_apps_no_lam : forall n (us : Tes n) u t, not_lam u -> apps u us =>b t -> exists v vs, t = apps v vs /\ clos_vaeq beta (Vcons u us) (Vcons v vs).
proof: Proof. intros n us u t hu b. inversion b; subst. destruct (apps_aeq_l H) as [v [vs [h1 [h2 h3]]]]; subst. rewrite <- h2 in hu. destruct (beta_apps_no_lam hu H1) as [w [ws [i1 i2]]]; subst. destruct (apps_aeq_r H0) as [c [cs [j1 [j2 j3]]]]; subst. exists c. exists cs. intuition. symmetry in h2, h3, j2, j3. exists (Vcons v vs). split. fo. exists (Vcons w ws). intuition. fo. Qed.
imports: Coq(Wf_nat Basics Morphisms) CoLoR(RelUtil LogicUtil VecUtil VecOrd SN NatUtil)