type bool ::= true |

false

op a : bool = (op true : bool)

op notA : bool = case (op a : bool) of true : bool ->

(op false : bool) |

false : bool -> (op true : bool)

op b : bool = let x : bool = (op true : bool);

y : bool = (op false : bool);

z : bool = (var x : bool) in (op true : bool)

op b : bool -> bool = \ x : bool . (var x : bool)

%% Type Constructors -----------------------------------------------------

Pred : Type -> Type := \ a : Type . a ->? Unit

Unit : Type := Unit

bool : Type %[type __ ::=

true : -> __

false : -> __]%

%% Assumptions -----------------------------------------------------------

__/\__ : Unit � Unit ->? Unit

__<=>__ : Unit � Unit ->? Unit

__=__ : forall a : Type . a � a ->? Unit

__=>__ : Unit � Unit ->? Unit

__=e=__ : forall a : Type . a � a ->? Unit

__\/__ : Unit � Unit ->? Unit

a : bool = (op true : bool)

b : bool -> bool = \ x : bool . (var x : bool)

: bool = let x : bool = (op true : bool);

y : bool = (op false : bool);

z : bool = (var x : bool) in (op true : bool)

def__ : forall a : Type . a ->? Unit

false : bool %(construct bool)%

if__then__else__ : forall a : Type . Unit � a � a ->? a

not__ : Unit ->? Unit

notA : bool = case (op a : bool) of true : bool ->

(op false : bool) |

false : bool -> (op true : bool)

true : bool %(construct bool)%