proposition: Lemma singleton_subst_term_noSubst : forall M G T (MG: correct_subst M G), isSingletonSubst T G -> activeEnv M |= 0 :! -> term M = term (subst MG).
proof: Proof. intros. set (MT := singleton_correct_single MG H). rewrite <- (singleton_subst MT MG); trivial. apply (@singleton_subst_term_noSubst_aux M T 0); trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)