proposition: Lemma singleton_subst M P G (CS: correct_subst M {x/P}) (CS': correct_subst M G) : isSingletonSubst P G -> subst CS = subst CS'.
proof: Proof. intro. apply term_eq. autorewrite with terms using simpl. rewrite (subst_ran_singleton H). destruct (subst_dom_singleton H) as [E [DomG Eempty]]. rewrite DomG. destruct (env M); destruct (env P); try destruct o; try destruct o0; try_solve; autorewrite with terms using simpl; try rewrite (env_sub_Empty e Eempty); try_solve. autorewrite with terms. unfold presubst. apply (singleton_presubst M 0 0 H). Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)