Something

Given in untyped lambda-calculus is the eta-rule:
\l x . Mx --> M , (x not free in M)

let G be defined as:
G \equiv \l xy . y(xy)

Proof that for every (closed) term H the following statement holds:
' H is a fixed-point-combinator if and only if H is a fixed point of G '