let dep jl = 
  match !proofmode with
    | No -> Atom.Set.empty
    | Dep -> List.fold_left Atom.Set.union Atom.Set.empty jl