fact: Definition activeEnv_compSubst_on M N x y := forall A, activeEnv M |= x := A <-> activeEnv N |= y := A.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)