proposition: Lemma equiv_hole_l : forall E k p, p < k -> equiv E p (initialSeg E k ++ finalSeg E (S k)) p.
proof: Proof. intros; unfold equiv, VarD, VarUD. destruct (le_gt_dec (length E) p). assert (p >= length (initialSeg E k ++ finalSeg E (S k))). autorewrite with datatypes using simpl. lia. split; split; intro; try solve [left; apply nth_beyond; trivial]. set (ww := nth_some E p H1); lia. exfalso; apply varD_UD_absurd with (initialSeg E k ++ finalSeg E (S k)) p A; trivial. left; apply nth_beyond; trivial. unfold VarD, VarUD. rewrite !nth_app_left, initialSeg_nth; fo. autorewrite with datatypes. apply Nat.min_case; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)