4Use of this equality is often referred to as η-conversion or η-expansion.