Software Foundations Ch. 7 Coq exercises

By popular demand, we're working on a new cycle of Software Foundations (https://softwarefoundations.cis.upenn.edu/current/index.html).

Let's do the Coq exercises for chapter 7 (Inductively Defined Propositions), and discuss.

The Coq proof assistant is central to the whole ecosystem for verified software that is being developed under the NSF Deep Specification initiative. Software Foundations is an online text in principles of verified software from a type-theoretic point of view, emphasizing hands-on work with Coq.

The university has apparently tightened parking enforcement. If you arrive after 6 p.m., a free 2-hour visitor parking permit should be enough, but it is required to have one for any time before 8 p.m.