let apply f p a =
    let (b, rho) = f a in   (* [rho |- a = b] *)
      match p b with
        | (Some(tau) as res) ->      (* [tau |- p(b)] *)
            if a == b then res else 
              Some(dep2 tau rho)
        | None ->
            None