es62

Se J fosse definibile allora avremmo nel lambda-calcolo che 
false <-- (\x.false)y <-- (\x.Jxy)y --> Jyy --> true 
cioe' true = false, cioe' due forme normali beta convertibili, impossibile.