proposition: Lemma subst_proof_irr M G (C1 C2: correct_subst M G) : subst C1 = subst C2.
proof: Proof. apply term_eq. rewrite !subst_env; trivial. rewrite !subst_term; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)