proposition: Lemma equiv_hole_r : forall E k p p', p > k -> p = S p' -> equiv E p (initialSeg E k ++ finalSeg E (S 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' - Nat.min k (length E)) with (p' - k). split; split; intro; solve [ replace (S k + (p' - k)) with (S p'); [trivial | lia] | replace (S p') with (S k + (p' - k)); [trivial | lia] ]. rewrite Nat.min_l; lia. replace (p' - Nat.min k (length E)) with (p' - (length E)). split; split; intro; 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. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)