let map f ((a, rho) as fct) =
  match Atom.atom_of a with
    | Atom.TT -> fct
    | Atom.FF -> fct
    | Atom.Equal(a, b) ->
        let a', tau = f a
        and b', sigma = f b in
          if a == a' && b == b' then fct else
            (Atom.mk_equal (a', b'), Jst.dep3 rho tau sigma)
    | Atom.Diseq(a, b) ->
        let a', tau = f a
        and b', sigma = f b in
          if a == a' && b == b' then fct else
            (Atom.mk_diseq (a', b'), Jst.dep3 rho tau sigma)
    | Atom.Nonneg(a) ->
        let a', tau = f a in
          if a == a' then fct else
            (Atom.mk_nonneg a', Jst.dep2 rho tau)
    | Atom.Pos(a) ->
        let a', tau = f a in
          if a == a' then fct else
            (Atom.mk_pos a', Jst.dep2 rho tau)