proposition: Lemma envSubst_transp_lift : forall S, envSubst_transp (envSubst_lift1 S) <=> envSubst_lift1 (envSubst_transp S).
proof: Proof. intros; constructor; intros i j; destruct S; destruct i; destruct j; fo. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)