proposition: Lemma betaStep_subst_stable : forall M N G (MS: correct_subst M G) (NS: correct_subst N G), BetaStep M N -> BetaStep (subst MS) (subst NS).
proof: Proof. intros M N G MS NS MN. inversion MN. set (MNS_app := app_subst_app Mapp0 MS). assert (MNS_Labs: isAbs (appBodyL MNS_app)). eapply abs_isAbs. assert (MS_term : term (subst MS) = presubst_aux (term (appBodyL Mapp0)) 0 G [presubst_aux (term (appBodyR Mapp0)) 0 G]). rewrite subst_term; term_inv M. rewrite (appBodyL_term (subst MS) MS_term). rewrite (abs_term (appBodyL Mapp0) MLabs). simpl; eauto. rewrite (beta_lower_subst Mapp0 MLabs MS NS MNS_Labs); auto. constructor. Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)