let dep1 j =
  match !proofmode with
    | No -> Atom.Set.empty
    | Dep -> j