proposition: Lemma app_beta_args : forall M N f, isApp M -> M -b-> N -> term (appHead M) = ^f -> exists l, exists el, isArg (fst el) M /\ isArg (snd el) N /\ fst el -b-> snd el /\ appArgs M = fst l ++ fst el::snd l /\ appArgs N = fst l ++ snd el::snd l.
proof: Proof. destruct M as [E Pt T TypM]. induction TypM; try solve [intros; inversion H]. intros N f Mapp MbetaN Mhead. inversion MbetaN; try contr. inversion H. exfalso. apply beta_direct_funApp with (buildT (TApp TypM1 TypM2)) Mapp1; eauto with terms. simpl in *. rewrite (appHead_app (buildT (TApp TypM1 TypM2)) I) in Mhead; trivial. case (isApp_dec (buildT TypM1)). intro M1app. destruct (IHTypM1 (appBodyL Napp) f) as [[al ar] [[tl tr] [tlM [trN [tltr [Margs Nargs]]]]]]; simpl in *; trivial. exists (al, ar ++ appBodyR Napp::nil); exists (tl, tr); repeat split; simpl; trivial. apply appArg_left with I; trivial. apply appArg_left with Napp; trivial. rewrite (appArgs_app (buildT (TApp TypM1 TypM2)) I); simpl. rewrite Margs; rewrite H0. rewrite <- ass_app; auto with datatypes. rewrite (appArgs_app N Napp); simpl. rewrite Nargs. rewrite <- ass_app; auto with datatypes. intro M1nApp; simpl in *. rewrite appHead_notApp in Mhead; simpl in Mhead. exfalso. apply beta_notFunS with (buildT TypM1) (appBodyL Napp); eauto with terms. trivial. term_inv N. exists (appArgs (buildT TypM1), nil(A:=Term)). exists (buildT TypM2, buildT T2); repeat split; simpl; trivial. apply appArg_right with I; trivial. apply appArg_right with I; trivial. rewrite appArgs_app with (buildT (TApp TypM1 TypM2)) I; trivial. rewrite appArgs_app with Tr I. rewrite H0; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)