proposition: Lemma subst_arg : forall M Marg G (MG: correct_subst M G), isArg Marg M -> exists MGarg, isArg MGarg (subst MG) /\ exists MargG: correct_subst Marg G, MGarg = subst MargG.
proof: Proof. intro M. apply well_founded_ind with (R := subterm) (P := fun M => forall Marg G (MG: correct_subst M G), isArg Marg M -> exists MGarg, isArg MGarg (subst MG) /\ exists MargG: correct_subst Marg G, MGarg = subst MargG). apply subterm_wf. clear M; intros M IH Marg G MG MargM. destruct (isApp_dec M) as [Mapp | Mnapp]. set (MG_app := app_subst_app Mapp MG). destruct (app_subst Mapp MG) as [MGl MGr]. destruct (appArg_inv M Marg Mapp MargM) as [argL | argR]. destruct (IH (appBodyL Mapp) (appBodyL_subterm M Mapp) Marg G (subst_appL_c Mapp MG) argL) as [W [WL [MargG WMargG]]]. exists W; split. apply appArg_left with MG_app. unfold MG_app; rewrite MGl; trivial. exists MargG; trivial. exists (appBodyR MG_app); split. apply appArg_right with MG_app; trivial. rewrite argR. exists (subst_appR_c Mapp MG); trivial. absurd (isArg Marg M); trivial. unfold isArg; rewrite appArgs_notApp; try_solve. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)