Six weeks ago, I proved a theorem about Plotkin's PCF (the proto-language behind Haskell and ML) which settles an open problem of 20 years' standing. This is also probably the first theorem I've ever proved whose content would be readily accessible to anyone who has taken (and understood) the Informatics 1 Functional Programming course. I will explain the statement of the result, and say a little about its proof.