Manuscript Oai276-A@1 · Oai276-A.tex · section · 215068af
The external claims, not local premises
Stage 0: freeze the channel, units, and claims › The external claims, not local premises · lines 375–379
Neither external record is assumed in the proof of Theorem thm:finite-certificate.