proposition: Lemma envSubst_lower_lift : forall Q, envSubst_lower (envSubst_lift1 Q) <=> Q.
proof: Proof. intros; destruct Q; fo. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)