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


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