proposition: Lemma initialSeg_prefix : forall (l: list A) x p el, nth_error (initialSeg l x) p = Some el -> nth_error l p = Some el.
proof: Proof. induction l; intros. destruct x; trivial. destruct x. destruct p; discr. inversion H. destruct p; trivial. rewrite H1. simpl; apply IHl with x; trivial. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)