erased α is the same as α, except that the elements of erased α are erased in the VM in the same way as types and proofs. This can be used to track data without storing it literally.