let inj =
  let la = Some(la)
  and p = Some(p)
  and bv = Some(bv)
  and cop = Some(cop)
  and nl = Some(nl)
  and app = Some(app)
  and arr = Some(arr)
  and u = Some(u)
  and set = Some(set) in
    function
      | Shostak(i) -> (match i with APP -> app | LA -> la | P -> p | BV -> bv | COP -> cop | SET -> set)
      | Can(i) -> (match i with ARR -> arr | NL -> nl)
      | Uninterpreted -> u