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

AB :: Set
   = sig{a :: A;b :: B;}

CD :: Set
   = sig{c :: C; d :: D;}

f (a_c:: A->C)
  (b_d:: B->D)
  (ab:: AB)
  :: CD
  = open ab use a,b
      in
      let c'::C = a_c a
          d'::D = b_d b
      in  struct{c = c';d = d'}