fact: Record correct_subst (M: Term) (G: Subst) : Prop := { envs_c: subst_envs_comp G; dom_c: subst_dom G [<->] env M; ran_c: subst_ran G [-] subst_dom G [<->] env M }.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)