proposition: Lemma singleton_subst_activeEnv_noSubst_aux : forall M T i (MG: correct_subst M (copy i None ++ Some T :: nil)), activeEnv M |= i :! -> activeEnv M = activeEnv (subst MG).
proof: Proof. destruct M as [E Pt T M]; induction M; intros. simpl. assert (MGterm: term (subst MG) = %x). autorewrite with terms using unfold presubst; simpl. destruct (lt_eq_lt_dec x i) as [[x_i | x_i] | x_i]. rewrite nth_app_left; autorewrite with datatypes using trivial. exfalso; apply (@varD_UD_absurd (copy i None ++ A [#] EmptyEnv) x A). unfold VarD, EmptyEnv, decl. rewrite x_i; apply nth_after_copy. simpl in H. rewrite x_i; rewrite x_i in H; trivial. rewrite nth_app_right; autorewrite with datatypes using (try lia). cut (x - i > 0). destruct (x - i). intros; lia. destruct n; trivial. lia. rewrite (activeEnv_var (subst MG) MGterm). autorewrite with terms; trivial. rewrite activeEnv_funS; simpl; trivial. rewrite activeEnv_funS; trivial. apply funS_is_funS with f. change (^f) with (term (buildT (TFun E f))). apply funS_presubst; simpl; trivial. set (MG_abs := abs_subst_abs (M := buildT (TAbs M)) I MG). assert (eqin: activeEnv (buildT M) = activeEnv (absBody MG_abs)). destruct (abs_subst (M:=buildT (TAbs M)) I MG). unfold MG_abs; rewrite H1. assert (MG': correct_subst (buildT M) (copy (S i) None ++ {x/lift T 1})). set (w := subst_abs_c (M:=buildT (TAbs M)) I MG). simpl in w. rewrite lift_subst_app in w. rewrite lift_empty_subst in w; trivial. replace (subst (subst_abs_c (M:=buildT (TAbs M)) I MG)) with (subst MG'). apply IHM. apply varUD_tail_rev; trivial. apply term_eq. rewrite !subst_env, !lift_subst_app, !lift_empty_subst. autorewrite with terms datatypes using simpl; trivial. autorewrite with datatypes terms. rewrite lift_subst_app. autorewrite with datatypes terms using simpl; trivial. rewrite (activeEnv_abs (buildT (TAbs M)) I). rewrite (activeEnv_abs (subst MG) MG_abs). rewrite <- eqin; trivial. rewrite (activeEnv_app (buildT (TApp M1 M2)) I). rewrite (activeEnv_app (subst MG) (app_subst_app (M:=buildT (TApp M1 M2)) I MG)). destruct (app_subst (M := buildT (TApp M1 M2)) I MG). rewrite H0; rewrite H1. unfold appBodyL; cbv beta. unfold appBodyR; cbv beta. rewrite (@activeEnv_app (buildT (TApp M1 M2)) I) in H. rewrite (IHM1 T i (subst_appL_c (M:=buildT (TApp M1 M2)) I MG)). rewrite (IHM2 T i (subst_appR_c (M:=buildT (TApp M1 M2)) I MG)); trivial. apply env_sumn_rn with (activeEnv (buildT M1)); trivial. apply env_sumn_ln with (activeEnv (buildT M2)); trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)