proposition: Lemma envSubst_transp_def : forall p q Q, envSub Q p q -> envSub (envSubst_transp Q) q p.
proof: Proof. intros; destruct Q; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)