proposition: Lemma equiv_copy_split_l : forall E k p n, p < k -> equiv E p (initialSeg E k ++ copy n None ++ finalSeg E k) p.
proof: Proof. intros; unfold equiv. destruct (le_gt_dec (length E) p). set (w := split_beyond E n H l). split; split; intro; trivial. set (ww := nth_some E p H0); lia. exfalso; apply varD_UD_absurd with (initialSeg E k ++ copy n None ++ finalSeg E k) p A; trivial. left; apply nth_beyond; trivial. unfold VarD, VarUD. rewrite !nth_app_left, initialSeg_nth; fo. autorewrite with datatypes. apply Nat.min_case; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)