[ For some work formalizing a reflection principle in HOL, see https://intelligence.org/files/ProofProducingReflection.pdf ]