Wilmer Ricciotti's solution

• Authors: Wilmer Ricciotti
• Parts addressed: 1a
• Proof assistant / theorem prover used: Matita.
• Encoding technique: Locally nameless.
• Files: available from the author's page.

Commentary

• This solution was meant as a test case for the Matita, an interactive theorem prover currently under development at the University of Bologna.
• A first version of the solution followed closely Leroy's swap-based approach.
• The current version of the solution follows closely the specifications, through the use of a hybrid inversion/induction principle.
• A formalization of the proof of adequacy for the locally nameless encoding is also provided.