fact: Definition subst_aux : forall (M: Term) (G: Subst) (C: correct_subst M G), {Q: Term | env Q = env M [-] subst_dom G [+] subst_ran G /\ term Q = presubst (term M) G /\ type Q = type M }.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)