fact: Fixpoint Vin (x : A) n (v : vector A n) : Prop := match v with | Vnil => False | Vcons y w => y = x \/ Vin x w end.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)