Reduce using eta-equivalence

[TurtlePU]

After enabling the corresponding option (see #9), terms should be evaluated with respect to both beta-reduction and eta-equivalence. Term is in eta-normal form iff it does not contain subterm of a form \x -> M x.