proposition: Lemma app_subst M (Mapp: isApp M) G (S: correct_subst M G) (SL : correct_subst (appBodyL Mapp) G := subst_appL_c Mapp S) (SR : correct_subst (appBodyR Mapp) G := subst_appR_c Mapp S) (Sapp : isApp (subst S) := app_subst_app Mapp S) : appBodyL Sapp = subst SL /\ appBodyR Sapp = subst SR.
proof: Proof. split; apply term_eq. autorewrite with terms; trivial. term_inv M. rewrite subst_term; simpl. assert (Mterm: term (subst S) = presubst PtL G @@ presubst PtR G). rewrite subst_term; trivial. rewrite (appBodyL_term (subst S) Mterm); trivial. autorewrite with terms; trivial. term_inv M. rewrite subst_term; simpl. assert (Mterm: term (subst S) = presubst PtL G @@ presubst PtR G). rewrite subst_term; trivial. rewrite (appBodyR_term (subst S) Mterm); trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)