proposition: Lemma loweredEnv_var_notLowered : forall E x A k, E |= k :! -> E |= x := A -> k > x -> loweredEnv E k |= x := A.
proof: Proof. intros E x A k Ek0 Ex kx. unfold VarD, loweredEnv. rewrite nth_app_left. rewrite initialSeg_nth; trivial. rewrite initialSeg_length; trivial. apply Nat.min_case; trivial. rewrite_lr (nth_in E x); unfold VarD in Ex; try_solve. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)