17:19
@user21820 What is your approach for proving the drinker's paradox?
What I struggle with in a lot of these proofs is that it seems like proving that something exists (so far) has not been using exists-intro but rather proof by contradiction
Maybe this one is different though