Conjecture: If your password is not correct, you will be redirected to a non-existing page (Setzer 2008).
Disproof. Formalise as . We want to prove , where is the type of passwords, is true iff is the correct password and means we are redirected to a void by .
Suppose . holds, where , thus we must have . However by the true constructive meaning of , namely typing the password into the form and observing the result—redirection to http://www.cs.swan.ac.uk/~csetzer/index.html—we can conclude , which may be written . From and we get by arrow-elimination, thus we can discharge our assumption. QED.