証明を static な木として記述させるとして、証明済みの定理をどうやって適用させるかがなかなか悩ましい。一番単純にいくなら、証明済みの定理をそのままコピーすることのみを許可する方法かな・・・