proposition: Lemma singleton_subst_activeEnv_noSubst M G T (MG: correct_subst M G) : activeEnv M |= 0 :! -> isSingletonSubst T G -> activeEnv M = activeEnv (subst MG).
proof: Proof. intros. set (MT := singleton_correct_single MG H0). rewrite <- (singleton_subst MT MG H0). change {x/T} with (copy 0 None ++ {x/T}) in MT. apply (singleton_subst_activeEnv_noSubst_aux T MT); trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)