let equality s x =
  let (a, prf) = justification s x in
    Fact.mk_equal x a prf