A reifier that emits the certificate along with the AST #

Lean2Js/Denotes.lean has one lemma per syntactic form; this is the metaprogram that walks an author's def and pastes them together. The AST and the proof are built in the same pass, so a rule can never be applied to the AST without its lemma being applied to the proof — that is what "the reifier is not trusted" means in code.

The three rules a refusal closes with #

A refusal that cannot name what to write instead names the rule the term broke, and there are three: what a value may be, whose vocabulary it reads, and where a call may go. The first two are the first rule of the subset reference, said of the types and of the names; Lean2Js.Denote pins the wording, so neither side can move alone.