The file hw08.elf has the language from class, but extended with the static and dynamic semantics for pairs and projections - this means that the progress proof is no longer correct, because it is missing the cases for pairs! Fill in the three missing lemmas and the missing cases of the proof, which will allow you to uncomment the %total declarations that have been commented out.
Feel free to check out the Homework 3 solution in Twelf for an example of many more progress proof. However, if you have the previous versions of this solution that included a partial solution for pairs, kindly ignore that!
Assignment 3 involved doing the preservation, not progress, theorem for pairs. Progress for pairs was covered in your notes for October 8, in Chapter 11 of Pierce's book, and Chapter 17 of the current draft of Bob Harper's book.