let apply f p a b =
    let (a', alpha') = f a in   (* [alpha' |- a = a'] *)
    let (b', beta') = f b in     (* [beta' |- b = b'] *)
      match p a' b' with
        | None -> None
        | (Some(tau) as res) ->      (* [tau |- p a' b'] *)
            if a == a' && b == b' then res else
              Some(dep3 tau alpha' beta')