On Thu, Dec 18, 2014 at 12:28 PM, Pascal Knodel <pascal.knodel@mail.com> wrote:

> (∀ ys • (∀ f,zs • map f (ys ++ zs) = map f ys ++ map f zs))
>
> And now you can see that you want a proof of a one-variable theorem

Thank you, Rustom Mody, that's it, reordering of universal quantifiers.
By the way, I'm searching for a 'good' book about predicate logic for quite some time now.
One with a strong link to mathematics and the quantification style
that is used there would be nice. By chance, is there a reference (script/paper/book )
you would recommend?

Two predicate calculus books that are particularly my favorites:
1. Dijkstra and Scholtens Predicate Calculus and Program semantics (5th chapter is logic)

2. Logical Approach to Discrete Math by Gries and Schneider

Second is more of a student textbook

My own attempts (20 year old!) at integrating the Haskell philosophy with the Dijkstra style of logic described in these books is here:

http://blog.languager.org/2014/09/pugofer.html