状況のフィードバックがない：公理の表示

theoremなどを使って証明した最後に結果（定理のステートメントに対応する命題シェマ）が表示されるが、axiomatizationで公理を導入すると命題シェマが表示されない。find_theorems nama: コマンドを使う必要がある。

find_* コマンドを使って状況確認するってのが、徹底的にTTY的な発想だと思うが。