data True = true
data False = 

data Bool = tt | ff

and (a,b:: Bool)
    :: Bool
    = case a of
        (tt) -> case b of
                  (tt) -> tt
                  (ff) -> ff
        (ff) -> ff



atom (b:: Bool)
     :: Set
     = case b of
         (tt) -> True
         (ff) -> False

ProdBool :: Set
         = sig
             first :: Bool
             snd   :: Bool


f1 (pair :: ProdBool)
  (p    :: atom (and pair.first pair.snd))
  :: atom pair.first
  = case pair.first of
    (tt)->
      {!true!}
    (ff)->
      {!!}


h (a,b :: Bool)
  (p :: atom (and a b))
  :: atom a
  = case a of
    (tt)->
      true
    (ff)->
      case p of { }


f2 (pair :: ProdBool)
  (p    :: atom (and pair.first pair.snd))
  :: atom pair.first
  = h pair.first pair.snd p