Christian Urban et al.'s solution

• Authors: Christian Urban, Benjamin Pierce, Dimitris Vytiniotis, Stephanie Weirich, Steve Zdancewic, with help from Stefan Berghofer and Markus Wenzel
• Parts addressed: 1a.
• Proof assistant / theorem prover used: Isabelle/HOL.
• Encoding technique: Nominal.
• Files: available from the author's page. Look in the nominal datatype package under examples/fsub.thy.
• Generated documentation: [ps]