Timothy Jones, David J. Pearce: A Mechanical Soundness Proof for Subtyping Over Recursive Types. FTfJP@ECOOP 2016: 1