proposition: Lemma app_beta_args_eq : forall M N Q f, isApp M -> M -b-> N -> term (appHead M) = ^f -> isArg Q N -> (isArg Q M \/ (exists2 Mb, Mb -b-> Q & isArg Mb M)).
proof: Proof. intros M N Q f Mapp MbN Mhead QargN. destruct (app_beta_args Mapp MbN Mhead) as [[al ar] [[tl tr] [tlM [trN [tltr [Margs Nargs]]]]]]; simpl in * . unfold isArg in QargN; rewrite Nargs in QargN. destruct (in_app_or QargN). left. unfold isArg; rewrite Margs; auto with datatypes. inversion H. right; exists tl. rewrite <- H0; trivial. unfold isArg; rewrite Margs; auto with datatypes. left. unfold isArg; rewrite Margs; auto with datatypes. Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)