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