let equality s x =
  let (y, prf) = find s x in
    Fact.mk_equal x y prf