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