type bool ::= True | False

op a : bool = True

op notA : bool = case a of True -> False | False -> True

op b : bool = let x = True; y = False; z = x in True

op b : bool -> bool = \x .! x