Artifact associated with POPL '21 paper

This release contains Coq proofs for the type soundness proof described in Section 7.2 of the POPL 2021 paper "A Graded Dependent Type System with a Usage-Aware Semantics"