proposition: Lemma funS_subst M G (MG: correct_subst M G) : isFunS M -> (subst MG) ~ M.
proof: Proof. intro. exists emptyEnvSubst. constructor. term_inv M. rewrite funS_presubst; trivial. simpl; constructor. apply conv_env_empty. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)