proposition: Lemma singleton_subst_term_noSubst_aux : forall M T i (MG: correct_subst M (copy i None ++ {x/T})), activeEnv M |= i :! -> term M = term (subst MG).
proof: Proof. destruct M as [E Pt T M]; induction M; intros; autorewrite with terms using unfold presubst; simpl. destruct (lt_eq_lt_dec i x) as [[i_x | i_x] | i_x]. rewrite nth_app_right; autorewrite with datatypes using trivial; try lia. assert (x - i > 0). lia. destruct (x - i). lia. destruct n; simpl; trivial. exfalso; apply varD_UD_absurd with (activeEnv (buildT (TVar v))) x A. apply activeEnv_var_decl; trivial. rewrite <- i_x; trivial. rewrite nth_app_left; autorewrite with datatypes using trivial. trivial. set (sc := subst_abs_c (M:=buildT (TAbs M)) I MG). simpl in sc. replace (None :: lift_subst (copy i None ++ {x/T}) 1) with (copy (S i) None ++ {x/lift T 1}) in sc. rewrite subst_lift_subst. replace (lift_subst (None :: copy i None ++ {x/T}) 1) with (copy (S i) None ++ {x/lift T 1}). set (w := IHM (lift T 1) (S i) sc). rewrite subst_term in w. change Pt with (term (buildT M)). rewrite <- w; clear w; trivial. rewrite (@activeEnv_abs (buildT (TAbs M)) I) in H. change (absBody (M:=buildT (TAbs M)) I) with (buildT M) in H. destruct (activeEnv (buildT M)); try_solve. simpl; rewrite lift_subst_app; rewrite lift_empty_subst; trivial. simpl; rewrite lift_subst_app; rewrite lift_empty_subst; trivial. change PtL with (term (buildT M1)). change PtR with (term (buildT M2)). set (w := IHM1 T i (subst_appL_c (M:=buildT (TApp M1 M2)) I MG)). rewrite subst_term in w; unfold presubst in w; rewrite <- w; clear w. set (w := IHM2 T i (subst_appR_c (M:=buildT (TApp M1 M2)) I MG)). rewrite subst_term in w; unfold presubst in w; rewrite <- w; trivial. rewrite (activeEnv_app (buildT (TApp M1 M2)) I) in H. change (buildT M2) with (appBodyR (M:=buildT (TApp M1 M2)) I). eapply env_sumn_rn; eexact H. rewrite (activeEnv_app (buildT (TApp M1 M2)) I) in H. change (buildT M1) with (appBodyL (M:=buildT (TApp M1 M2)) I). eapply env_sumn_ln; eexact H. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)