reg009.lidr

> isAnyBy : (alpha -> Bool) -> (n : Nat ** Vect n alpha) -> Bool
> isAnyBy _ (_ ** Nil) = False
> isAnyBy p (_ ** (a :: as)) = p a || isAnyBy p (_ ** as)

> filterTagP : (p  : alpha -> Bool) ->
>              (as : Vect n alpha) ->
>              so (isAnyBy p (n ** as)) ->
>              (m : Nat ** (Vect m (a : alpha ** so (p a)), so (m > Z)))
> filterTagP {n = S m} p (a :: as) q with (p a)
>   | True  = (_
>              **
>              ((a ** believe_me oh)
>               ::
>               (fst (getProof (filterTagP p as (believe_me oh)))),
>               oh
>              )
>             )
>   | False = filterTagP p as (believe_me oh)