proposition: Lemma var_loweredEnv_var_lowered : forall E x A k, E |= k :! -> loweredEnv E k |= x := A -> k <= x -> E |= S x := A.
proof: Proof. unfold VarD, loweredEnv. intros E x A k Ek0 Ex kx. rewrite nth_app_right in Ex. rewrite initialSeg_length in Ex. destruct (le_gt_dec (length E) k). rewrite finalSeg_empty in Ex. destruct (x - Nat.min k (length E)); try_solve. lia. rewrite Nat.min_l in Ex. destruct (le_gt_dec (length E) (S x)). rewrite nth_beyond in Ex; try_solve. rewrite finalSeg_length. lia. rewrite (@finalSeg_nth_nth (option SimpleType) E (S k) (S x)). replace (S x - S k) with (x - k); trivial. lia. lia. rewrite initialSeg_length. set (w := Nat.le_min_l k (length E)). lia. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)