Interesting Rocq Problems

Following are some interesting problems, philosophical explorations, and just neat ideas implemented in the Rocq Prover.

• Omniscience - some friends and I debated whether omniscience is impossible. Of course, omniscience isn't a well-defined property, but I thought an interesting way to disprove it was by showing that there could exist no set containing only all of the true statements.