Hello, Your definition for Bool reminds me a bit of the definition for booleans in Robert Dockins pure, untyped lambda calculus evaluator: http://www.eecs.tufts.edu/~rdocki01/lambda/prelude.lam http://www.eecs.tufts.edu/~rdocki01/lambda.html j.