fact: Fixpoint Vopt_filter n (ks : vector nat n) p (xs : vector A p) := match ks in vector _ n return vector (option A) n with | Vnil => Vnil | Vcons k ks' => Vcons (match lt_dec k p with left h => Some (Vnth xs h) | _ => None end) (Vopt_filter ks' xs) end.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)