fact: Definition subst_envs_comp (G: Subst) : Prop := forall i j Ti Tj, G |-> i/Ti -> G |-> j/Tj -> env Ti [<->] env Tj.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)