[hyp0]

EDIT one danger with a library is it might have a theorem stronger than what you're trying to prove (and that you aren't convinced yet by). If it's applied automatically, it's not a convincing proof. (And the purpose here is to be convincing, not just to be correct).

The easy answer is for the user to only allow libraries that they've accepted.

I was thinking we might have an automatic check, that we never use a theorem which is stronger than the whole thing we're trying to prove - that is, which implies our whole proof). But that seems hard to check automatically (maybe undecidable in general).