postulate A:: Set
postulate B:: Set
postulate C:: Set

A2 :: Set
   = A -> A

A3 :: Set
   = A2 -> A2

a2 :: A2
   = \(x::A)-> x

a2' :: A2
    = a2

a3 :: A3
   = \(x::A2)-> {!A2 !}