data Bool = tt | ff

data True = true
data False = 

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


neg (b:: Bool)
    :: Bool
    = case b of
      (tt)-> ff
      (ff)-> tt

Lemma5aux (x:: Bool)
          :: Set
          = sig
              b :: Bool
              p :: b == (neg x)


Lemma5 :: Set
       = (a :: Bool) -> Lemma5aux a


lemma5 :: Lemma5
       = \(a::Bool)-> 
          case a of
          (tt)->  struct
                    b = ff
                    p = true
          (ff)->  struct
                    b = tt
                    p = true