= then have with facts = from facts and this . = by this .. = by standard from facts (have|show) φ = (have|show) φ using facts TIPS (1/3) standard: 自動証明メソッドの一つ。context から rule の引数になりうるものを集めて rule を適用する。 sorry 証明したことにして次に進むためのコマンド 証明したことにした式はfactとして使える oops 証明を打ち切るためのコマンド