ただ、実際の数学の教科書の証明を見ていると「○○の定理より〜」みたいな感じで、既存の定理を推論規則として使っている場面が良くあって、定理をただコピーするだけじゃなくて、推論規則として使えるようにするみたいな仕組みもあった方が便利そうなのだけど、定理が推論規則になるっていう状況があまりきちんと定義されていないような気がする