Proof-closure audit

The commands below reject proof placeholders and nonstandard axioms in the paper-facing theorem and its principal producer lemmas.

def commandAssert_only_standard_axioms_ : Lean.ParserDescr

Reject a declaration if its dependency closure contains a custom axiom.

Equations

• One or more equations did not get rendered due to their size.