proposition: Lemma lift_lowerEnvSubst : forall k s, envSubst_lift1 (lowerEnvSubst k s) <=> lowerEnvSubst (S k) (S s).
proof: Proof. intros k; constructor; intros i j. destruct i; destruct j; try_solve. destruct (eq_nat_dec (S k) 0); lia. destruct (eq_nat_dec (S k) (S i)); try_solve. destruct (le_gt_dec k i); try_solve; try lia. destruct (eq_nat_dec (S k) (S i)); try_solve. destruct (le_gt_dec k i); try_solve; try lia. destruct (eq_nat_dec k i); lia. destruct (eq_nat_dec k i); lia. destruct i; destruct j; try_solve. destruct (eq_nat_dec (S k) 0); lia. destruct (eq_nat_dec (S k) (S i)); try_solve. destruct (eq_nat_dec k i); try_solve. destruct (eq_nat_dec k i); try_solve. 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)