proposition: Lemma liftedEnv_var_notLifted : forall E x A k n, E |= x := A -> x < k -> liftedEnv n E k |= x := A.
proof: Proof. unfold VarD, liftedEnv. intros E x A k n Ex x_k. rewrite nth_app_left. rewrite initialSeg_nth; trivial. autorewrite with datatypes. apply (Nat.min_case k (length E)); trivial. rewrite_lr (nth_in E x). destruct (nth_error E x); discr. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)