Equivalent up to renaming of bound variables

• Lambda terms are considered equivalent under renaming of BOUND variables.
• ( lambda x . ( y x ) ) == ( lambda z . ( y z ) )
• A free variable may not become bound by renaming.
• ( lambda x . ( y x ) ) != ( lambda y . ( y y ) )