proposition: Lemma copy_split_l_varD : forall E k p n A, p < k -> E |= p := A -> (initialSeg E k ++ copy n None ++ finalSeg E k) |= p := A.
proof: Proof. intros. apply (proj1 (proj1 (equiv_copy_split_l E n H) A)); trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)