proposition: Lemma singleton_subst_activeEnv_subst : forall M G T (MG: correct_subst M G), isSingletonSubst T G -> (exists A, activeEnv M |= 0 := A) -> activeEnv (subst MG) [=] (None :: tail (activeEnv M)) [+] activeEnv T.
proof: Proof. intros. destruct H0 as [A M0A]. set (MT := singleton_correct_single MG H). rewrite <- (singleton_subst MT MG H). set (w := @singleton_subst_activeEnv_subst_aux M T 0 A MT). change (copy 0 None ++ {x/T}) with {x/T} in w. apply env_eq_trans with ((initialSeg (activeEnv M) 0 ++ None :: finalSeg (activeEnv M) 1) [+] activeEnv T). apply w; trivial. clear w. simpl; destruct (activeEnv T); rewrite finalSeg1_tail; apply env_eq_refl. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)