proposition: Lemma eq_term_arg_aux : forall M Marg M', isArg Marg M -> term M = term M' -> exists M'arg, isArg M'arg M' /\ term M'arg = term Marg.
proof: Proof. intro M. apply well_founded_ind with (R := subterm) (P := fun M => forall Marg M', isArg Marg M -> term M = term M' -> exists M'arg, isArg M'arg M' /\ term M'arg = term Marg). apply subterm_wf. clear M; intros M IH Marg M' MargM MM'term. set (Mapp := appArg_app M Marg MargM). assert (M'app: isApp M'). term_inv M; term_inv M'. destruct (appArg_inv M Marg Mapp); trivial. destruct (IH (appBodyL Mapp) (appBodyL_subterm M Mapp) Marg (appBodyL M'app) H) as [M'Larg [M'LargM' M'Larg_term]]. term_inv M; term_inv M'. exists M'Larg; split. apply appArg_left with M'app; trivial. term_inv M; term_inv M'. exists (appBodyR M'app); split. apply appArg_right with M'app; trivial. rewrite H; trivial. term_inv M; term_inv M'. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)