Andrew Gacek's solution

• Authors: Andrew Gacek
• Parts addressed: 1a and 2a. Part 3 would be conducted using the same specification but using a system such as Teyjus.
• Proof assistant / theorem prover used: Abella.
• Encoding technique: HOAS.
• Files: available from the Abella page: Part 1a Part 2a