In this assignment, you'll practice working with induction (dependent elimination) on natural numbers and start working with the equality type. The Pie exercises cover Chapter 7 and 8.
The Pie assignment should be completed by writing a definition for each claim, and then uncommenting the tests so that they all pass. Passing the tests is necessary, but not sufficient, for completing the exercise - you should also follow the instructions in the file.
Parts of this assignment are written by David Christiansen and used with permission.