'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]
