postulate A:: Set
postulate B:: Set

Lemma1 :: Set
       =  A -> (A -> B) -> B


lemma1 :: Lemma1
       = \(a::A)-> 
         \(ab:: A-> B) ->
         ab a


lemma1direct (a :: A)
             (ab:: A -> B)
             :: B
             = ab a 
             


And1 (A,B:: Set)
     ::Set
     = sig
         first  :: A
         second :: B

And2 (A,B:: Set)
     ::Set
     = data and (a:: A) (b:: B)


(/\) (A,B:: Set)
     ::Set
     = data and (a:: A) (b:: B)

lemma2a (ab:: And1 A B)
        :: And1 B A
        =  struct
             first  = ab.second
             second = ab.first


lemma2 (ab:: And2 A B ) 
       :: And2 B A
       = case ab of
         (and a b)->
           and@_ b a


(\/) (A,B:: Set)
     :: Set
     = data inl (a:: A) | inr (b:: B)

lemm3 (ab :: A \/ B)
      :: B \/ A
      = case ab of
        (inl a)->
          inr@_ a
        (inr b)->
          inl@_ b



data Bool = tt | ff

data True = true
data False = 

Not (A:: Set)
    :: Set
    = A -> False

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


Lemma4 :: Set
       = (a:: Bool) -> Not (a < a)
       

lemma4 :: Lemma4
       = \(a:: Bool) ->
         \(aa:: a < a) -> 
          case a of
          (tt)->
            case p of { }
          (ff)->
            case p of { }