proposition: Lemma liftedEnv_distr_sum_equiv : forall El Er n k, liftedEnv n (El [+] Er) k [=] liftedEnv n El k [+] liftedEnv n Er k.
proof: Proof. unfold liftedEnv; intros; split; intros p A D. destruct (nth_app _ _ _ D) as [[Dl cond] | [Dr cond]]. assert (p < k). rewrite initialSeg_length in cond. set (w := Nat.le_min_l k (length (El[+]Er))); lia. set (ElErD := initialSeg_prefix (El[+]Er) k p Dl). destruct (env_sum_varDecl El Er ElErD) as [[ElD ErND] | ErD]. apply env_sum_ly_rn. apply copy_split_l_varD; trivial. apply copy_split_l_varUD; trivial. apply env_sum_ry. apply copy_split_l_varD; trivial. destruct (nth_app _ _ _ Dr) as [[Drl cond'] | [Drr cond']]; rewrite copy_length in cond'. rewrite (@nth_copy_in (option SimpleType) n None (p - length (initialSeg (El[+]Er) k))) in Drl; try_solve. rewrite copy_length in Drr. set (ElErD := Drr); rewrite nth_finalSeg_nth in ElErD. assert (length (initialSeg (El[+]Er) k) = k). autorewrite with datatypes. destruct (le_gt_dec (length (El[+]Er)) k). rewrite finalSeg_empty in Drr; trivial. destruct (p - length (initialSeg (El[+]Er) k) - n); try_solve. apply Nat.min_l; lia. destruct (env_sum_varDecl El Er ElErD) as [[ElD ErND] | ErD]. apply env_sum_ly_rn. apply copy_split_r_varD with (k + (p - length (initialSeg (El[+]Er) k) - n)); trivial; try lia. apply copy_split_r_varUD with (k + (p - length (initialSeg (El[+]Er) k) - n)); trivial; try lia. apply env_sum_ry. apply copy_split_r_varD with (k + (p - length (initialSeg (El[+]Er) k) - n)); trivial; try lia. destruct (env_sum_varDecl _ _ D) as [[DL DRN] | DR]. destruct (nth_app _ _ _ DL) as [[DLl cond] | [DLr cond]]. assert (p < k). rewrite initialSeg_length in cond. set (w := Nat.le_min_l k (length El)). lia. apply copy_split_l_varD; trivial. apply env_sum_ly_rn. rewrite initialSeg_nth in DLl; trivial. apply copy_split_l_rev_varUD with k n; trivial. destruct (nth_app _ _ _ DLr) as [[DLrl cond'] | [DLrr cond']]; rewrite copy_length in cond'. rewrite (@nth_copy_in (option SimpleType) n None (p - length (initialSeg El k))) in DLrl; try_solve. assert (length (initialSeg El k) = k). autorewrite with datatypes. destruct (le_gt_dec (length El) k). rewrite finalSeg_empty in DLrr; trivial. rewrite copy_length in DLrr. destruct (p - length (initialSeg El k) - n); try_solve. apply Nat.min_l; lia. rewrite copy_length in DLrr. set (w := DLrr); rewrite nth_finalSeg_nth in w. apply copy_split_r_varD with (k + (p - length (initialSeg El k) - n)); trivial; try lia. apply env_sum_ly_rn; trivial. apply copy_split_r_rev_varUD with k n p; trivial; try lia. destruct (nth_app _ _ _ DR) as [[DRl cond] | [DRr cond]]. apply copy_split_l_varD; trivial. rewrite initialSeg_length in cond. set (w := Nat.le_min_l k (length Er)); lia. apply env_sum_ry. unfold VarD; apply initialSeg_prefix with k; trivial. destruct (nth_app _ _ _ DRr) as [[DRrl cond'] | [DRrr cond']]; rewrite copy_length in cond'. rewrite (@nth_copy_in (option SimpleType) n None (p - length (initialSeg Er k))) in DRrl; try_solve. rewrite copy_length in DRrr. set (w := DRrr); rewrite nth_finalSeg_nth in w. assert (length (initialSeg Er k) = k). autorewrite with datatypes. destruct (le_gt_dec (length Er) k). clear w. rewrite finalSeg_empty in DRrr; trivial. destruct (p - length (initialSeg Er k) - n); try_solve. apply Nat.min_l; lia. apply copy_split_r_varD with (k + (p - length (initialSeg Er k) - n)); trivial; try lia. apply env_sum_ry; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)