knuton/la-girafe-sportive — pull request #10 by yfyf (2013-12-12 02:00:06+00:00)
Title: Add η-conversion

Just the definition for now.

Also added the generic compatibility closure, but did not translate `bred` to use it. It works nicely, except for the annoying thing that you always have to do `apply clos_base. apply _base.` for the base cases, instead of just `apply clos_base.`

Perhaps this can be resolved with some coercion magic?