proposition: Lemma envSubst_lift_compose : forall S1 S2, envSubst_lift1 (envSubst_compose S1 S2) <=> envSubst_compose (envSubst_lift1 S1) (envSubst_lift1 S2).
proof: Proof. intros S1 S2; constructor; intros i j; destruct S1; destruct S2. destruct i; destruct j; fo; destruct x; fo. destruct i; destruct j; try_solve. exists 0; fo. destruct 1; exists (S x); trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)