proposition: Lemma env_subset_lowered : forall E E' n, envSubset E E' -> envSubset (loweredEnv E n) (loweredEnv E' n).
proof: Proof. intros; unfold loweredEnv; intros w A D. destruct (nth_app (initialSeg E n) (finalSeg E (S n)) w D) as [[ED w_len] | [ED w_len]]; rewrite initialSeg_length in w_len; try rewrite initialSeg_length in ED. assert (E' |= w := A). apply H; unfold VarD. apply initialSeg_prefix with n; trivial. assert (w < n). set (h := Nat.le_min_l n (length E)). lia. unfold VarD; rewrite nth_app_left; autorewrite with datatypes; trivial. apply Nat.min_case; trivial. apply nth_some with (Some A); trivial. assert (Nat.min n (length E) = n). apply Nat.min_l. set (h := finalSeg_nth_idx E (S n) (w - Nat.min n (length E)) ED). lia. rewrite H0 in ED. assert (ED': nth_error E (S n + (w - n)) = Some (Some A)). rewrite <- nth_finalSeg_nth; trivial. set (E'D := H (S n + (w - n)) A ED'). replace (S n + (w - n)) with (S w) in E'D. assert (Nat.min n (length E') = n). set (ww := nth_some E' (S w) E'D). apply Nat.min_l. lia. unfold VarD; rewrite nth_app_right. autorewrite with datatypes; rewrite H1. replace (S n + (w - n)) with (S w); trivial. lia. autorewrite with datatypes. rewrite H1; rewrite <- H0; trivial. lia. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)