'NimAudit.BinReadout.toNatBE_eq_iff' depends on axioms: [propext, Quot.sound] 'NimAudit.BinReadout.decodeC_eval' depends on axioms: [propext, Quot.sound] 'NimAudit.BinReadout.firstTrue_eqs' depends on axioms: [propext, Quot.sound] 'NimAudit.BinReadout.toRCirc_correct' depends on axioms: [propext, Quot.sound] 'NimAudit.BinReadout.getC_mem' depends on axioms: [propext] 'NimAudit.BinReadout.decodeC_resources' depends on axioms: [propext, Quot.sound] 'NimAudit.BinReadout.toRCirc_RBound' depends on axioms: [propext, Quot.sound] 'NimAudit.BinReadout.succCountRO_congr' depends on axioms: [propext, Classical.choice, Quot.sound] 'NimAudit.BinReadout.binary_readout_bound' depends on axioms: [propext, Classical.choice, Quot.sound] 'NimAudit.BinReadout.pad_boardBits' depends on axioms: [propext, Quot.sound] 'NimAudit.BinReadout.netBCirc_eval' depends on axioms: [propext, Classical.choice, Quot.sound] 'NimAudit.BinReadout.netReadout_eq' depends on axioms: [propext, Classical.choice, Quot.sound] 'NimAudit.BinReadout.netBCirc_BBound' depends on axioms: [propext, Classical.choice, Quot.sound] 'NimAudit.BinReadout.network_readout_bound' depends on axioms: [propext, Classical.choice, Quot.sound]