Stefan Berghofer's solution

• Author: Stefan Berghofer.
• Parts addressed: all.
• Proof assistant / theorem prover used: Isabelle/HOL.
• Encoding technique: DeBruijn.
• Files: available from the author's page.