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 <your-rel>_base.` for the base cases, instead of just `apply clos_base.`

Perhaps this can be resolved with some coercion magic?