proposition: Lemma liftedEnv_var_lifted : forall E x A k n, E |= x := A -> x >= k -> liftedEnv n E k |= x + n := A.
proof: Proof. intros E x A k n. unfold VarD, liftedEnv. intros E_x x_k. assert (x_E: x < length E). rewrite_lr (nth_in E x). destruct (nth_error E x); discr. assert (k_E: Nat.min k (length E) = k). apply Nat.min_l. lia. rewrite nth_app_right; autorewrite with datatypes. rewrite k_E. rewrite nth_app_right; autorewrite with datatypes. replace (k + (x + n - k - n)) with x; trivial. lia. lia. lia. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)