proposition: Lemma subst_arg_rev : forall M G MGarg (MG: correct_subst M G), isArg MGarg (subst MG) -> (exists Marg, isArg Marg M /\ exists MGin: correct_subst Marg G, MGarg = subst MGin) \/ (exists p T Targ, isArg Targ T /\ G |-> p / T /\ term MGarg = term Targ).
proof: Proof. intro M. apply well_founded_ind with (R := subterm) (P := fun M => forall G MGarg (MG: correct_subst M G), isArg MGarg (subst MG) -> (exists Marg, isArg Marg M /\ exists MGin: correct_subst Marg G, MGarg = subst MGin ) \/ (exists p, exists T, exists Targ, isArg Targ T /\ G |-> p / T /\ term MGarg = term Targ )). apply subterm_wf. clear M; intros M IH G MGarg MG MGargMG. destruct (term_case M) as [[[Mvar | Mfun] | Mabs] | Mapp]. destruct (var_subst MG Mvar) as [[T [p GpT MGterm]] | MGvar]. right; exists p; exists T. destruct (eq_term_arg_aux (subst MG) MGarg T) as [Targ [TargT TargMGarg]]; trivial. exists Targ; split; trivial. split; auto. assert (forall W, isVar W -> isApp W -> False). intro W; term_inv W. exfalso. apply H with (subst MG). term_inv M. apply var_is_var with x; rewrite MGvar; trivial. apply appArg_app with MGarg; trivial. assert (forall W, isFunS W -> isApp W -> False). intro W; term_inv W. exfalso. apply H with (subst MG); trivial. apply funS_subst_funS; trivial. apply appArg_app with MGarg; trivial. assert (forall W, isApp W -> isAbs W -> False). intro W; term_inv W. exfalso. apply H with (subst MG); trivial. apply appArg_app with MGarg; trivial. apply abs_subst_abs; trivial. destruct (app_subst Mapp MG). destruct (appArg_inv (subst MG) MGarg (app_subst_app Mapp MG)); trivial. destruct (IH (appBodyL Mapp) (appBodyL_subterm M Mapp) G MGarg (subst_appL_c Mapp MG)) as [[Marg [MargML [MGin MGargMGin]]] | [p [T [Targ [TargT [GpT MGarg_term]]]]]]. rewrite <- H; trivial. left; exists Marg; split. apply appArg_left with Mapp; trivial. exists MGin; trivial. right; exists p; exists T; exists Targ; split; trivial. split; trivial. left; exists (appBodyR Mapp); split. apply appArg_right with Mapp; trivial. exists (subst_appR_c Mapp MG). rewrite <- H0; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)