let merge e s =
  let (x, y, prf) = Fact.d_equal e in   (* [prf |- x = y] *)
  let (x', prf1) = find s x in          (* [prf1 |- x = x']. *)
  let (y', prf2) = find s y in          (* [prf2 |- y = y']. *)
  let (x', y') = Term.orient (x', y') in
    if Term.eq x' y' then 
      (Term.Set.empty, s)
    else
      let prf' = Fact.mk_rule "trans" [prf; prf1; prf2] in
        (Term.Set.singleton x', union x' y' prf' s)