let theory_of = function
    | App(f, _, _) -> Sym.theory_of f 
    | _ -> raise Not_found