Wilmer Ricciotti's solution
Parts addressed: 1a
Proof assistant / theorem prover used: Matita.
Encoding technique: Locally nameless.
Files: available from the
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.