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