proposition: Lemma loweredEnv_distr_sum_equiv : forall El Er n, loweredEnv (El [+] Er) n [=] loweredEnv El n [+] loweredEnv Er n.
proof: Proof. unfold loweredEnv; intros; split; intros p A D. destruct (nth_app _ _ _ D) as [[Dl cond] | [Dr cond]]. assert (p < n). rewrite initialSeg_length in cond. set (w := Nat.le_min_l n (length (El[+]Er))); lia. set (ElErD := initialSeg_prefix (El[+]Er) n p Dl). destruct (env_sum_varDecl El Er ElErD) as [[ElD ErND] | ErD]. apply env_sum_ly_rn. apply hole_l_varD; trivial. apply hole_l_varUD; trivial. apply env_sum_ry. apply hole_l_varD; trivial. set (ElErD := Dr); rewrite nth_finalSeg_nth in ElErD. assert (length (initialSeg (El[+]Er) n) = n). autorewrite with datatypes. destruct (le_gt_dec (length (El[+]Er)) n). clear ElErD. rewrite finalSeg_empty in Dr; trivial. destruct (p - length (initialSeg (El[+]Er) n)); try_solve. lia. apply Nat.min_l; lia. destruct (env_sum_varDecl El Er ElErD) as [[ElD ErND] | ErD]. apply env_sum_ly_rn. apply hole_r_varD with (S n + (p - length (initialSeg (El[+]Er) n))); trivial; try lia. apply hole_r_varUD with (S n + (p - length (initialSeg (El[+]Er) n))); trivial; try lia. apply env_sum_ry. apply hole_r_varD with (S n + (p - length (initialSeg (El[+]Er) n))); trivial; try lia. destruct (env_sum_varDecl _ _ D) as [[DL DRN] | DR]. destruct (nth_app _ _ _ DL) as [[DLl cond] | [DLr cond]]. assert (p < n). rewrite initialSeg_length in cond. set (w := Nat.le_min_l n (length El)). lia. apply hole_l_varD; trivial. apply env_sum_ly_rn. rewrite initialSeg_nth in DLl; trivial. apply hole_l_rev_varUD with n; trivial. assert (length (initialSeg El n) = n). autorewrite with datatypes. destruct (le_gt_dec (length El) n). rewrite finalSeg_empty in DLr; trivial. destruct (p - length (initialSeg El n)); try_solve. lia. apply Nat.min_l; lia. rewrite nth_finalSeg_nth in DLr. apply hole_r_varD with (S n + (p - length (initialSeg El n))); trivial; try lia. apply env_sum_ly_rn; trivial. apply hole_r_rev_varUD with n p; trivial; try lia. destruct (nth_app _ _ _ DR) as [[DRl cond] | [DRr cond]]. apply hole_l_varD. rewrite initialSeg_length in cond. set (w := Nat.le_min_l n (length Er)); lia. apply env_sum_ry. unfold VarD; apply initialSeg_prefix with n; trivial. set (w := DRr); rewrite nth_finalSeg_nth in w. assert (length (initialSeg Er n) = n). autorewrite with datatypes. destruct (le_gt_dec (length Er) n). rewrite finalSeg_empty in DRr; trivial. destruct (p - length (initialSeg Er n)); try_solve. lia. apply Nat.min_l; lia. apply hole_r_varD with (S n + (p - length (initialSeg Er n))); trivial; try lia. apply env_sum_ry; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)