proposition: Lemma beta_lower_subst : forall M N G (Mapp: isApp M) (MLabs: isAbs (appBodyL Mapp)) (MN: correct_subst M G) (NS: correct_subst N G) (MNS_app: isApp (subst MN) := app_subst_app Mapp MN) (MNS_Labs: isAbs (appBodyL MNS_app)), N = lower (subst (beta_subst M Mapp MLabs)) (beta_lowering M Mapp MLabs) -> subst NS = lower (subst (beta_subst (subst MN) MNS_app MNS_Labs)) (beta_lowering (subst MN) MNS_app MNS_Labs).
proof: Proof. intros. set (s0 := correct_subst_lift (subst (beta_subst M Mapp MLabs)) (beta_lowering M Mapp MLabs) NS H). rewrite (lower_subst (beta_lowering M Mapp MLabs) NS s0 H). apply lower_eq. assert (s1: correct_subst (absBody MLabs) (None :: lift_subst G 1)). inversion MN; inversion NS; inversion s0; prove_correct_subst. assert (s2: correct_subst (lift (appBodyR Mapp) 1) (None :: lift_subst G 1)). inversion MN; inversion NS; inversion s0; prove_correct_subst. assert (s3: correct_subst (subst s1) {x/subst s2}). constructor. apply subst_envs_comp_single. assert (forall E, {x/type (appBodyR Mapp)} [<->] Some (absType MLabs) :: E). intro; apply env_comp_cons. auto with terms. left; rewrite beta_type; trivial. destruct (subst_empty_dec G); autorewrite with terms using simpl; auto. destruct (subst_empty_dec G); autorewrite with terms datatypes using simpl; auto with terms. rewrite (double_subst G (beta_subst M Mapp MLabs) s0 s1 s2 s3). apply term_eq. destruct (subst_empty_dec G); autorewrite with datatypes terms using simpl; trivial. autorewrite with datatypes terms using simpl. assert (Leq: presubst (term (absBody MLabs)) (None :: lift_subst G 1) = term (absBody MNS_Labs)). cut (term (subst s1) = term (absBody MNS_Labs)). autorewrite with terms. intro; rewrite H0; trivial. rewrite (subst_on_beta Mapp MLabs MN s1 MNS_Labs); trivial. assert (R'eq: subst (subst_appR_c Mapp MN) = appBodyR MNS_app). destruct (app_subst Mapp MN). rewrite <- H1. rewrite (app_proof_irr (subst MN) (app_subst_app Mapp MN) MNS_app); trivial. assert (Req: subst s2 = lift (appBodyR MNS_app) 1). rewrite (double_lift s2 (subst_appR_c Mapp MN)). rewrite R'eq; trivial. try_solve. Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)