proposition: Lemma emptySubst_neutral : forall M S (CS: correct_subst M S), isEmptySubst S -> subst CS = M.
proof: Proof. intros; apply term_eq. rewrite subst_env; simpl. rewrite subst_ran_empty; trivial. rewrite env_sum_empty_r. rewrite env_sub_Empty; trivial. apply subst_dom_Empty; trivial. rewrite subst_term. apply empty_presubst_neutral. intros p pS. destruct p; trivial. destruct (list_In_nth S (Some t) pS). destruct (H x); try_solve. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)