let sigma f al =
  match Sym.get f with
    | Sym.Arith(op) ->  Arith.sigma op al
    | Sym.Product(op) -> Product.sigma op al
    | Sym.Bv(op) ->  Bitvector.sigma op al
    | Sym.Coproduct(op) -> Coproduct.sigma op al
    | Sym.Propset(op) -> Propset.sigma op al
    | Sym.Cl(op) -> Apply.sigma op al
    | Sym.Pp(op) -> Pprod.sigma op al
    | Sym.Uninterp _ -> Term.App.mk_app f al
    | Sym.Arrays(op) -> Funarr.sigma Term.is_equal op al