是否有一种方法可以将提示数据库中的所有引理添加到核心中，这样我就不必继续在文件中的任何地方编写auto with foo？
auto with foo
Hint Resolve 1 => solve [ auto with foo ] : core.