As someone who's spent many, many hours proving things in Coq, I concur with the original post--pointfree stuff is usually much less easy to read than the same function with named variables. A lot of that comes down to not being able to tell what's going on at all if you don't already know the arity of the functions you're using.