The Coq scripts compile with the command make, using coqc --version 8.4pl6 (July 2015).

• dsubsup_total.v -- termination proof for D<:> as described in the submission (Section 3)
• dsubsup_total_alt.v -- alternative proof for D<:> plus recursive self types and intersection types (see artifact guide below)

An artifact guide is available here (PDF), which describes the correspondence with the paper as well as the new alternative proof.