'UltravioletChain.activity_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.hbeta_of_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.small_field_mass_of_rarity' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.small_field_mass_invariant' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.expectation_diff_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.split_small_field' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.gauge_choice' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.equicontinuous_of_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.vanishing_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.vanishing_linear' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.chain_to_hypotheses' depends on axioms: [propext, Classical.choice, Quot.sound]
