On Exercise 2 don’t worry about the “guessing decreasing argument” issue the Coq type checker brings up. When I wrote the exam I did not anticipate anyone trying to actually code the tree structure up in the prover because it was intended to be done in class. Assume that Coq can find the decreasing argument. There is a solution to this, but it’s not what I want you spending your time on.