Alberto Ciaffaglione and Ivan Scagnetto's solution

• Authors: Alberto Ciaffaglione and Ivan Scagnetto
• Parts addressed: 1a.
• Proof assistant / theorem prover used: Coq.
• Encoding technique: Weak higher-order abstract syntax.
• Files: Available from the author's page.