fact: Fixpoint vapp {A n m} (v : vector A n) (w : vector A m) : vector A (n + m) := match v with | nil => w | cons a v' => cons a (vapp v' w) end.
imports: Program Bvector List Relations Equations.Prop.Equations Utf8 Arith Wf_nat Vectors.Vector Bvector