Axiom audit

Compiler-visible axiom reports for the public theorem, retained supporting results, and the graded-interval proof. Each report must use only propext, Classical.choice, and Quot.sound.

Additional theorems of the graded-interval development