proposition: Lemma var_liftedEnv_var_notLifted : forall E x A k n, liftedEnv n E k |= x := A -> x < k -> E |= x := A.
proof: Proof. unfold VarD, liftedEnv. intros E x A k n Ex x_k. destruct (le_gt_dec k (length E)). rewrite nth_app_left in Ex. rewrite <- (initialSeg_nth E x_k); trivial. autorewrite with datatypes. rewrite Nat.min_l; trivial. destruct (le_gt_dec (length E) x). rewrite nth_app_right in Ex. rewrite initialSeg_length in Ex. rewrite Nat.min_r in Ex; [trivial | lia]. rewrite finalSeg_empty in Ex; trivial. rewrite <- app_nil_end in Ex. destruct (le_gt_dec (length (copy n (A := option SimpleType) None)) (x - length E)). set (w := nth_beyond (copy n None) l0); try_solve. assert (x - length E < n). rewrite copy_length in g0. trivial. set (w := nth_copy_in (A:=option SimpleType) (n:=n) None H); try_solve. lia. autorewrite with datatypes. rewrite Nat.min_r; trivial. lia. rewrite nth_app_left in Ex. rewrite <- (initialSeg_nth E x_k); trivial. autorewrite with datatypes. rewrite Nat.min_r; lia. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)