proposition: Lemma Vforall_map_elim : forall A B (f: A->B) (P : B->Prop) n (v : vector A n), Vforall P (Vmap f v) -> Vforall (fun a : A => P (f a)) v.
proof: Proof. induction v; simpl; intuition. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)