let inv (s, p) a = 
    try
      let i = Sym.theory_of (Term.App.sym_of a) in
        (match i with
          | Th.Uninterpreted -> 
              Jst.Eqtrans.compose (Partition.find p) (U.S.inv s.u) a
          | Th.Shostak(i) -> 
              (match i with
                 | Th.LA -> La.S.inv s.la a
                 | Th.BV -> S.inv s.bv a
                 | Th.P -> S.inv s.p a
                 | Th.COP -> S.inv s.cop a
                 | Th.APP -> S.inv s.cl a 
                 | Th.SET -> S.inv s.set a)
          | Th.Can(i) ->
              (match i with
                 | Th.NL -> Nl.Ops.inv (p, s.nl) a
                 | Th.ARR -> Nl.Ops.inv (p,s .arr) a))
    with
        Not_found -> Partition.find p a