proposition: Lemma eq_vec_dec : forall n (v1 v2 : vector A n), {v1=v2}+{~v1=v2}.
proof: Proof. induction v1; intro. VOtac. auto. VSntac v2. case (eq_dec h (Vhead v2)); intro. rewrite e. case (IHv1 (Vtail v2)); intro. rewrite e0. auto. right. unfold not. intro. Veqtac. auto. right. unfold not. intro. Veqtac. auto. Defined.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)