proposition: Lemma subst_term M G (C: correct_subst M G) : term (subst C) = presubst (term M) G.
proof: Proof. unfold subst; intros. destruct (subst_aux C); simpl; tauto. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)