'RegularityStep.abs_prod_sub_prod_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityStep.pointwise_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityStep.expectation_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityStep.equicontinuous_of_small_field' depends on axioms: [propext, Classical.choice, Quot.sound]
'CThetaReadings.hessian_reading_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'CThetaReadings.hessian_reading_theta_max' depends on axioms: [propext, Classical.choice, Quot.sound]
'CThetaReadings.coefficient_reading_04' depends on axioms: [propext, Classical.choice, Quot.sound]
'CThetaReadings.coefficient_reading_068' depends on axioms: [propext, Classical.choice, Quot.sound]
'CThetaReadings.minimizer_lipschitz' depends on axioms: [propext, Classical.choice, Quot.sound]
'CThetaReadings.K_bg_mono' depends on axioms: [propext, Classical.choice, Quot.sound]
'CThetaReadings.K_bg_value' depends on axioms: [propext, Classical.choice, Quot.sound]
'HessianGap.flux_one_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'HessianGap.flux_two_planes' depends on axioms: [propext, Classical.choice, Quot.sound]
'HessianGap.flux_three_planes' depends on axioms: [propext, Classical.choice, Quot.sound]
'HessianGap.flux_six' depends on axioms: [propext, Classical.choice, Quot.sound]
'HessianGap.flux_self_dual' depends on axioms: [propext, Classical.choice, Quot.sound]
'HessianGap.flux_nonabelian' depends on axioms: [propext, Classical.choice, Quot.sound]
'HessianGap.flux_complex' depends on axioms: [propext, Classical.choice, Quot.sound]
'HessianGap.cov_points' depends on axioms: [propext, Classical.choice, Quot.sound]
'HessianGap.mix06_points' depends on axioms: [propext, Classical.choice, Quot.sound]
'HessianGap.straight_point' depends on axioms: [propext, Classical.choice, Quot.sound]
'HessianGap.uniform_in_f1' depends on axioms: [propext, Classical.choice, Quot.sound]
'HessianGap.f1_edges' depends on axioms: [propext, Classical.choice, Quot.sound]
'HessianGap.gap_at_04' depends on axioms: [propext, Classical.choice, Quot.sound]
'HessianGap.K_bg_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'HessianGap.equicontinuous_from_gap' depends on axioms: [propext, Classical.choice, Quot.sound]
'HessianGap.K_bg_uniform' depends on axioms: [propext, Classical.choice, Quot.sound]
