postulate A :: Set
postulate a:: A
postulate f:: A -> Set

g  (a:: A)
   :: A
   = a

a' :: A
   = g a

p  (x :: f a)
   :: (f a')
   = {! !}