Add combinator examples

Also intend to show that `Y t` is a fixpoint of `t` (by showing it reduces to `t (Y t)`). For this I need eta-conversion, though.

Plus, need to fix how `dename` handles unbound variables, and am not yet sure how to best do this. I could first analyse the depth of the term, but even then, how to decide which number to assign to which unbound formula?