proposition: Lemma funS_presubst M G (MG: correct_subst M G) : isFunS M -> term (subst MG) = term M.
proof: Proof. intros. term_inv M. rewrite subst_term. compute; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)