'TwoStageSmallField.UltravioletChain.activity_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.hbeta_of_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.small_field_mass_of_rarity' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'TwoStageSmallField.UltravioletChain.small_field_mass_invariant' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'TwoStageSmallField.UltravioletChain.expectation_diff_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.split_small_field' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.gauge_choice' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.equicontinuous_of_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.vanishing_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.vanishing_linear' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.chain_to_hypotheses' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.badSet_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.goodSet_eq_compl' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.block_bad_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.block_bad_le_counts' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.index_bad_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.index_good_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.small_field_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.eta_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.small_field_two_stage_box' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.rarity_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.chain_hypotheses_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.hsf_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]
