let find (s, p) = function
    | Th.Uninterpreted -> 
        Jst.Eqtrans.id  (* no find for uninterpreted theory. *)
    | Th.Shostak(i) -> 
        (match i with
           | Th.LA -> La.S.find s.la
           | Th.BV -> S.find s.bv
           | Th.P -> S.find s.p
           | Th.COP -> S.find s.cop
           | Th.APP -> S.find s.cl
           | Th.SET -> S.find s.set)
    | Th.Can(i) ->
        (match i with
           | Th.NL -> Nl.Ops.find (p, s.nl)
           | Th.ARR -> (Nl.Ops.find (p, s.arr)))