postulate A:: Type 
postulate B:: Type 
postulate C:: Type 

BC :: Type
   = sig{b :: B;
         c :: C}


f :: (A -> BC) -> A -> B
  =  \(x::A -> BC) -> \(a::A) -> let bc :: BC
                                       = x a
                                 in  bc.b