concatMap' : (Monoid v) => (l : List a) -> ((le : a) -> Data.List.Elem le e -> v) -> v
concatMap' [] f = neutral
concatMap' (x :: xs) f = f x Here <+> (concatMap' xs (\el, p => f el $ There p))