proposition: Lemma equiv_copy_split_r : forall E k n p p', p >= k -> p' = p + n -> equiv E p (initialSeg E k ++ copy n None ++ finalSeg E k) p'.
proof: Proof. intros; unfold equiv, VarD, VarUD; rewrite H0. rewrite !nth_app_right; autorewrite with datatypes. destruct (le_gt_dec k (length E)). replace (p + n - Nat.min k (length E) - n) with (p - k). split; split; intro; solve [ replace (k + (p - k)) with p; [trivial | lia] | replace p with (k + (p - k)); [trivial | lia] ]. rewrite Nat.min_l; lia. replace (p + n - Nat.min k (length E) - n) with (p - length E). split; split; intro; try solve [ left; apply nth_beyond; lia | set (w := nth_some E _ H1); lia ]. rewrite Nat.min_r; lia. set (w := Nat.le_min_l k (length E)); lia. set (w := Nat.le_min_l k (length E)); lia. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)