let symb_def =
  let rec loop acc system = match system with
    | [] -> acc
    | (Term(f,_),_) :: system -> loop (SymbSet.add f acc) system
    | _ -> failwith "not possible"
  in loop SymbSet.empty system