proposition: Lemma Veq_nth : forall n (v v' : vector A n), (forall i (ip : i < n), Vnth v ip = Vnth v' ip) -> v = v'.
proof: Proof. induction n; intros. VOtac. refl. VSntac v. VSntac v'. apply Vcons_eq_intro. rewrite !Vhead_nth. apply H. apply IHn. intros. rewrite !Vnth_tail. apply H. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)