The encoding of booleans in pure lambda calculus:
true := λx.λy.x
false := λx.λy.y
cond := λb.λx.λy.b x y
So if "cond" re-defined as cond := λx.x and assume "true" and "false" are keep same as before, does this result in a valid encoding of booleans?