let rec to_string th =
  match th with
    | Shostak(i) -> shostak_to_string i
    | Can(i) -> can_to_string i
    | Uninterpreted -> "u"

and shostak_to_string i =
  match i with
    | LA -> "la"
    | P -> "p"
    | BV -> "bv"
    | COP -> "cop"
    | SET -> "pset"
    | APP -> "cl"

and can_to_string i =
  match i with
    | NL -> "nl"
    | ARR -> "arr"