André Hirschowitz and Marco Maggesi's solution

• Authors: André Hirschowitz and Marco Maggesi
• Parts addressed: 1a.
• Proof assistant / theorem prover used: Coq.
• Encoding technique: Nested Abstract Syntax.
• Files: Available from the author's page.