'NimAudit.ClassicalBoundary.aoDepth_and' depends on axioms: [propext, Quot.sound]
'NimAudit.ClassicalBoundary.aoDepth_or' depends on axioms: [propext, Quot.sound]
'NimAudit.ClassicalBoundary.aoGates_and' depends on axioms: [propext, Quot.sound]
'NimAudit.ClassicalBoundary.aoGates_or' depends on axioms: [propext, Quot.sound]
'NimAudit.ClassicalBoundary.negLeaf_and' depends on axioms: [propext, Quot.sound]
'NimAudit.ClassicalBoundary.negLeaf_or' depends on axioms: [propext, Quot.sound]
'NimAudit.ClassicalBoundary.nnf_and' depends on axioms: [propext, Quot.sound]
'NimAudit.ClassicalBoundary.nnf_or' depends on axioms: [propext, Quot.sound]
'NimAudit.ClassicalBoundary.any_not_eq' depends on axioms: [propext]
'NimAudit.ClassicalBoundary.all_not_eq' depends on axioms: [propext]
'NimAudit.ClassicalBoundary.eval_nnf' depends on axioms: [propext, Quot.sound]
'NimAudit.ClassicalBoundary.negLeaf_nnf' depends on axioms: [propext, Quot.sound]
'NimAudit.ClassicalBoundary.listMax_map_congr' depends on axioms: [propext, Quot.sound]
'NimAudit.ClassicalBoundary.sum_map_congr'' depends on axioms: [propext, Quot.sound]
'NimAudit.ClassicalBoundary.aoDepth_nnf' depends on axioms: [propext, Quot.sound]
'NimAudit.ClassicalBoundary.aoGates_nnf' depends on axioms: [propext, Quot.sound]
'NimAudit.ClassicalBoundary.maxInput_nnf' depends on axioms: [propext, Quot.sound]
'NimAudit.ClassicalBoundary.aoDepth_le' depends on axioms: [propext, Quot.sound]
'NimAudit.ClassicalBoundary.aoGates_le' depends on axioms: [propext, Quot.sound]
'NimAudit.ClassicalBoundary.dnf_aoDepth' depends on axioms: [propext, Quot.sound]
'NimAudit.ClassicalBoundary.sgn_not'' depends on axioms: [propext]
'NimAudit.ClassicalBoundary.sgn_par_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.ClassicalBoundary.indicator_signed' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.ClassicalBoundary.classicalCorr_mono' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.ClassicalBoundary.classicalCorr_mono_d' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.ClassicalBoundary.hastadNegl_of_deep' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.ClassicalBoundary.premise_of_classical' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.ClassicalBoundary.premise_mono' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.ClassicalBoundary.parityNotAC0_of_hastad' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.ClassicalBoundary.rsum_nonneg'' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.ClassicalBoundary.term_le_rsum' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.ClassicalBoundary.pow_cast_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.ClassicalBoundary.term_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.ClassicalBoundary.rsum_count_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.ClassicalBoundary.half_le_self' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.ClassicalBoundary.le_one_of_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.ClassicalBoundary.pow_two_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.ClassicalBoundary.etaSum_negligible' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.ClassicalBoundary.uparE_eval' does not depend on any axioms
'NimAudit.ClassicalBoundary.upar_poly' depends on axioms: [propext, Quot.sound]
'NimAudit.ClassicalBoundary.netE_eval' does not depend on any axioms
'NimAudit.ClassicalBoundary.netsize_poly' depends on axioms: [propext, Quot.sound]
'NimAudit.ClassicalBoundary.search_gap_asymptotic' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.ClassicalBoundary.search_gap_asymptotic_net' depends on axioms: [propext, Classical.choice, Quot.sound]