let sigma f =
  match f with
    | Sym.Arith(op) -> Arith.sigma op
    | Sym.Pair(op) -> Pair.sigma op
    | Sym.Bv(op) -> Bitvector.sigma op
    | Sym.Coproduct(op) -> Coproduct.sigma op
    | Sym.Fun(op) -> Apply.sigma op
    | Sym.Pp(op) -> Pp.sigma op
    | Sym.Bvarith(op) -> Bvarith.sigma op
    | Sym.Arrays(op) -> Arr.sigma Term.is_equal op
    | Sym.Uninterp _ -> Term.mk_app f