appendix sectionsignatures

Checked front-end edges

Nuprl card $⇝$ quotient card.: A locally proved PER extension, not an artifact-verified closure constructor.
Timpl $\leftarrow T_{elab}$ .: Elaboration removes surface omissions and contextual metavariables; the solved target is independently rechecked. Soundness is relative to the named conversion interface.
Timpl $\leftarrow$ Timpl-clauses.: Successful compilation removes patterns in favor of eliminators. The local typing and closed-data simulation theorems justify this translation only for the frozen clause card.