fact: Fixpoint Vfilter n (bs : bools n) : vec n -> vec (Vtrue bs) := match bs as bs in vector _ n return vec n -> vec (Vtrue bs) with | Vnil => fun _ => Vnil | Vcons true bs' => fun v => Vcons (Vhead v) (Vfilter bs' (Vtail v)) | Vcons false bs' => fun v => Vfilter bs' (Vtail v) end.
imports: Coq(Arith) CoLoR(VecUtil LogicUtil EqUtil)