Axiom report for the public theorem and simple count

Every declaration below must depend only on propext, Classical.choice, and Quot.sound. The larger supporting-result report is AxiomAudit.