let extend i e s =
  let (x, a, prf) = Fact.d_equal e in
    assert(not (mem s x));
    union i e s