Adam Chlipala's solution

• Author: Adam Chlipala.
• Parts addressed: 1a.
• Proof assistant / theorem prover used: Coq.
• Encoding technique: Locally nameless.
• Files: available from the author's page.