proposition: Lemma loweredEnv_var_lowered : forall E x A k, E |= k :! -> E |= x := A -> k <= x -> loweredEnv E k |= pred x := A.
proof: Proof. intros E x A k Ek0 Ex k_x. assert (x_E: x < length E). rewrite_lr (nth_in E x); unfold VarD in Ex; try_solve. destruct (proj1 (Nat.lt_eq_cases _ _) k_x) as [k_lt_x | k_eq_x]. destruct x. lia. unfold VarD, loweredEnv. rewrite nth_app_right. unfold finalSeg; simpl. destruct E; try_solve. assert (k_E: Nat.min k (S (length E)) = k). rewrite Nat.min_l; lia. rewrite seg_nth. rewrite initialSeg_length; simpl. rewrite k_E. replace (k + (x - k)) with x; solve [trivial | lia]. rewrite initialSeg_length; simpl. rewrite k_E; lia. rewrite initialSeg_length. rewrite Nat.min_l; lia. rewrite k_eq_x in Ek0. unfold VarD in Ex; destruct Ek0; try_solve. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)