AnnoDomini in Practice: A Type-Theoretic Approach to the Year 2000 Problem