let dep i s =
    match i with
      | Th.Uninterpreted -> 
          U.S.dep s.u
      | Th.Shostak(i) -> 
          (match i with
             | Th.LA -> La.S.dep s.la
             | Th.BV -> S.dep s.bv
             | Th.P -> S.dep s.p
             | Th.COP -> S.dep s.cop
             | Th.APP -> S.dep s.cl
             | Th.SET -> S.dep s.set)
      | Th.Can(i) ->
          (match i with
             | Th.NL -> S.dep s.nl
             | Th.ARR -> S.dep s.arr)