proposition: Lemma lift_liftEnvSubst : forall n k s, envSubst_lift1 (liftEnvSubst n k s) <=> liftEnvSubst n (S k) (S s).
proof: Proof. intros n k s; constructor; intros i j. destruct i; destruct j; try_solve; try lia. destruct (le_gt_dec k i); try_solve; try lia. destruct (le_gt_dec k i); try_solve; try lia. destruct i; destruct j; try_solve; try lia. destruct (le_gt_dec k i); try_solve; lia. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)