let sym_of a = 
  assert(is_app a);
  match a with App(f,_) -> f | _ -> assert false