postulate A:: Set
postulate B:: Set

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


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