The least equality on lambda terms closed under lambda application and lambda abstraction and containing beta equivalence and eta conversion, with bound names identified by alpha equivalence.
New to topics? Read the docs here!
New to topics? Read the docs here!