proposition: Lemma Vforall_app : forall p (v : vector A p) q (w : vector A q), Vforall (Vapp v w) <-> Vforall v /\ Vforall w.
proof: Proof. induction v; fo. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)