knuton/la-girafe-sportive — pull request #9 by knuton (2013-12-12 00:19:04+00:00)
Title: 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?