proposition: Lemma beta_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 /\ Vcons u us -->b Vcons v vs.
proof: Proof. induction us; simpl; intros u t hu b. exists t. exists Vnil. intuition. apply left_sym. hyp. assert (k : not_lam (App u h)). discr. destruct (IHus _ _ k b) as [v [vs [h1 h2]]]. inversion h2; subst. inversion H0; subst. inversion H; subst. exfalso. eapply hu. refl. exists u'. exists (Vcons h vs). intuition. apply left_sym. hyp. exists u. exists (Vcons v' vs). intuition. apply right_sym. apply left_sym. hyp. exists u. exists (Vcons h vs). intuition. do 2 apply right_sym. hyp. Qed.
imports: Coq(Wf_nat Basics Morphisms) CoLoR(RelUtil LogicUtil VecUtil VecOrd SN NatUtil)