Edit: Ah, and the Software Foundations books are amazing. I did a little course on formal verification during 2020 and learned a ton. Now every time I work with some kind of type system, I feel frustrated that I can't express everything that I want to in my type system.
It starts with the general rules of lambda calculus, then build up some basic functions (like in the PDF linked in this thread) and continues to build data types like Natural Numbers, List, String, Tree and operators for manipulating them. The book also explains about the evaluation methods as well as covering how ML and LISP uses lambda calculus.
> Y combinator: Y = λt. (λx. t (x x)) (λx. t (x x))
Edit: It was the Omega operator that did that.
where id = λx. x
(though Y Y does not normalize either, infinite looping like omega)