proposition: Lemma subst_on_beta : forall M (Mapp: isApp M) (MLabs: isAbs (appBodyL Mapp)) G (CS: correct_subst M G) (CSin: correct_subst (absBody MLabs) (None :: lift_subst G 1)) (CSapp: isApp (subst CS) := app_subst_app Mapp CS) (CSLabs: isAbs (appBodyL CSapp)), subst CSin = absBody CSLabs.
proof: Proof. intros; apply term_eq. assert (absType MLabs = absType CSLabs). apply type_eq_absType_eq. unfold CSapp; apply type_appBodyL_subst. destruct (subst_empty_dec G); autorewrite with terms using unfold decl; try_solve. autorewrite with terms datatypes using simpl. rewrite (absBody_term (appBodyL CSapp) CSLabs (A := absType MLabs) (Pt := presubst (term (absBody MLabs)) (None :: lift_subst G 1))); trivial. rewrite (appBodyL_term (subst CS) (PtL := \absType MLabs => presubst (term (absBody MLabs)) (None::lift_subst G 1)) (PtR := presubst (term (appBodyR Mapp)) G)); trivial. autorewrite with terms. rewrite (app_term M Mapp). rewrite (abs_term (appBodyL Mapp) MLabs). unfold presubst; simpl. rewrite subst_lift_subst; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)