proposition: Lemma subst_eq M M' G (MG: correct_subst M G) (MG': correct_subst M' G) : M = M' -> subst MG = subst MG'.
proof: Proof. intro M_M'. apply term_eq. rewrite !subst_env, M_M'; trivial. rewrite !subst_term, M_M'; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)