I have 0 experience with theorem provers (and almost 0 with proofs in general) but am at least somewhat aware of their existence. This might be the first time I feel like I can actually follow the code. Might start learning Oak because of this post, so thanks!