proposition: Lemma Vforall_dec : forall n (v : vector A n), {Vforall v}+{~Vforall v}.
proof: Proof. induction n; intros. VOtac. left. constructor. VSntac v. destruct (P_dec (Vhead v)). destruct (IHn (Vtail v)). left. simpl. split; hyp. right. intro V. destruct V. contr. right. intro V. destruct V. contr. Defined.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)