:l Empty.pi
:l Unit.pi

Bool : Type;
Bool = { true false };

T : Bool -> Type;
T = \ b -> case b of {
             true -> Unit
	   | false -> Empty };

andb : Bool -> Bool -> Bool;
andb = \ b c -> case b of {
                  true -> c
                | false -> 'false };