つーか，でかい証明を書くにはtacticsとかtacticalsが重要．
実際に証明を書いて見れ．