'NimAudit.Prob.rsum_nil' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.rsum_cons' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.rsum_append' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.rsum_congr' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.rsum_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.rsum_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.rsum_mul_left' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.rsum_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.rsum_const' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.rsum_comm' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.rsum_map' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.rsum_flatMap' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.rsum_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.rsum_range_ite' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.rsum_range_split0' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.range_one_add' depends on axioms: [propext, Quot.sound]
'NimAudit.Prob.rsum_offZero_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.rsum_offZero_const' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.rsum_offZero_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.rsum_offZero_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.mem_boards' depends on axioms: [propext, Quot.sound]
'NimAudit.Prob.rsum_boards_succ' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.count_boards' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.xor_eq_iff' depends on axioms: [propext, Quot.sound]
'NimAudit.Prob.sigma_uniform' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.dotB_xor_right' depends on axioms: [propext, Quot.sound]
'NimAudit.Prob.dotB_xor_left' depends on axioms: [propext, Quot.sound]
'NimAudit.Prob.dotB_zero_left' depends on axioms: [propext, Quot.sound]
'NimAudit.Prob.dotB_congr_left' depends on axioms: [propext, Quot.sound]
'NimAudit.Prob.chi_xor_right' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.chi_zero_left' depends on axioms: [propext, Quot.sound]
'NimAudit.Prob.chi_cases' depends on axioms: [propext]
'NimAudit.Prob.lowZero_spec' depends on axioms: [propext, Quot.sound]
'NimAudit.Prob.lowZero_iff' depends on axioms: [propext, Quot.sound]
'NimAudit.Prob.orthogonality' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.indicator_expansion' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.successB_iff' depends on axioms: [propext, Quot.sound]
'NimAudit.Prob.nimSum_set' depends on axioms: [propext, Quot.sound]
'NimAudit.Prob.set_move' depends on axioms: [propext]
'NimAudit.Prob.success_legal' depends on axioms: [propext]
'NimAudit.Prob.invalid_output' depends on axioms: [propext]
'NimAudit.Prob.success_iff_gval' depends on axioms: [propext, Quot.sound]
'NimAudit.Prob.q_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.T_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.T_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.rsum_boards_eq_T' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.div_mul_cancel'' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.div_le_div_of_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.le_div_of_mul_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.sigma_lt' depends on axioms: [propext, Quot.sound]
'NimAudit.Prob.Csum_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.natCast_pred' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.exact_value_count' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.exact_value_error' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.offZero_rsum' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.rsum_offZero_indicator' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.rsum_range_indicator_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.succCount_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.disjoint_le_two' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.C0_sum_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.succCount_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.nonzeroCount_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.prob_sigma_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.success_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.dotB_two_pow' depends on axioms: [propext, Quot.sound]
'NimAudit.Prob.head_linear' depends on axioms: [propext, Quot.sound]
'NimAudit.Prob.headVec_ne_zero' depends on axioms: [propext, Quot.sound]
'NimAudit.Prob.headVec_lt' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.rollout_outcome_linear' depends on axioms: [propext, Quot.sound]
'NimAudit.Prob.single_policy_affine' depends on axioms: [propext, Quot.sound]
'NimAudit.Prob.structured_head_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.negligible_const_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Prob.asymptotic_bound' depends on axioms: [propext, Classical.choice, Quot.sound]