Typecheck Bool.
Typecheck true.
Typecheck false.

Typecheck (\x. ! x).
Simpl (! true).
Simpl (! false).

Typecheck (\x. \y. x && y).
Simpl (false && false).
Simpl (true && false).
Simpl (false && true).
Simpl (true && true).

Typecheck (\x. \y. x || y).
Simpl (false || false).
Simpl (true || false).
Simpl (false || true).
Simpl (true || true).

Simpl ((\x. \y. x == y) true true).