On Thu, Dec 18, 2014 at 12:28 PM, Pascal Knodel
(∀ 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