proposition: Lemma var_loweredEnv_var_notLowered : forall E x A k, E |= k :! -> loweredEnv E k |= x := A -> k > x -> E |= x := A.
proof: Proof. unfold VarD, loweredEnv. intros E x A k Ek0 Ex kx. destruct (le_gt_dec (length E) x). destruct (le_gt_dec k (length E)). rewrite nth_app_left in Ex; trivial. rewrite <- (initialSeg_nth E kx); trivial. autorewrite with datatypes. apply Nat.min_case; lia. rewrite nth_app_right in Ex. rewrite finalSeg_empty in Ex. destruct (x - length (initialSeg E k)); try_solve. lia. autorewrite with datatypes. rewrite Nat.min_r; trivial. lia. rewrite nth_app_left in Ex. rewrite initialSeg_nth in Ex; trivial. autorewrite with datatypes. apply Nat.min_case; lia. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)