  Let us agree to abbreviate \([\lambda x\,[\lambda y\,X](g)](f)\) by \([\lambda xy\,X](f, g)\), when convenient. Suppose \(f\) is intended to be the intension of “the morning star,” and \(g\) is intended to be the intension of “the evening star.” Presumably \(f\) and \(g\) are distinct intensions. Even so, \([\lambda xy\,x = y]\)(f, g) is correct in the real world—both \(f\) and \(g\) do designate the same object.