thm 定理名 というコマンドで定理＝ルールを表示できるが、存在しない定理名を指定すると、Undefined fact と出る。ということは、実装上は、既存の定理をfactと呼んでいるようだ。print_statement 定理名 というコマンドで表示されるのは、定理名（ラベル）…