let compose f g a =
    let b, rho = g a in           (* [rho |- a = b] *)
    let c, tau = f b in           (* [tau |- b = c] *)
      (c, dep2 rho tau)