proposition: Lemma uneffective_singleton_subst_conv M G T (MG: correct_subst M G) : isSingletonSubst T G -> (activeEnv M |= 0 :!) -> terms_conv M (subst MG).
proof: Proof. intros. apply terms_conv_criterion_strong. apply singleton_subst_activeEnv_noSubst with T; trivial. apply singleton_subst_term_noSubst with T; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsSubst) Coq(Arith Lia)