Hongwei Xi's solution

• Authors: Hongwei Xi
• Parts addressed: 2a and 3. Part 2b is "thought to be straightforward". It is not clear whether part 1 is possible.
• Proof assistant / theorem prover used: ATS/LF.
• Encoding technique: combination of HOAS and de Bruijn indices.
• Files: [ats]