proposition: Lemma var_liftedEnv_var_lifted : forall E x A k n, liftedEnv n E k |= x + n := A -> x >= k -> E |= x := A.
proof: Proof. unfold VarD, liftedEnv. intros E x A k n Ex x_k. assert (x < length E). set (q := initialSeg E k ++ copy n None ++ finalSeg E k). assert (nth_error q (x + n) <> None). unfold q; try_solve. set (w := proj1 (nth_in q (x + n)) H). assert (length q = length E + n). unfold q. do 2 rewrite length_app. rewrite Nat.add_comm. rewrite <- Nat.add_assoc. rewrite (Nat.add_comm (length (finalSeg E k)) (length (initialSeg E k))). rewrite initialFinalSeg_length. autorewrite with datatypes using lia. rewrite H0 in w; lia. rewrite nth_app_right in Ex. rewrite initialSeg_length in Ex. destruct (le_lt_dec k (length E)). rewrite nth_app_right in Ex. rewrite copy_length in Ex. rewrite Nat.min_l in Ex; trivial. rewrite (finalSeg_nth_nth E x_k). replace (x - k) with (x + n - k - n); trivial. lia. autorewrite with datatypes. rewrite Nat.min_l; trivial. lia. lia. autorewrite with datatypes. destruct (le_gt_dec k (length E)). rewrite Nat.min_l; solve [trivial | lia]. lia. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)