let sym_theory_of f = Th.to_int (Th.of_sym f)