単なるループは定理証明で混ぜて使えないのも入れといて