Objectives:

1. Implement interpreter for the Type NS languages in Willard 2017.

2. Formalize the proof of non-diagonalizability for Type NS languages in a stronger metalanguage, Idris/Coq/Agda/etc.

3. Formalize as much of the proof in (2) as possible in a Type NS language itself, co-eval with determining whether/to what extent this can be done.

Claim: (3) would provide autonomous confidence in the consistency of the system so proved to be, by closing over the metatheory.