'SmallRemKernel.UltravioletChain.activity_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.hbeta_of_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.small_field_mass_of_rarity' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.small_field_mass_invariant' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.expectation_diff_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.split_small_field' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.gauge_choice' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.equicontinuous_of_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.vanishing_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.vanishing_linear' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.chain_to_hypotheses' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.small_rem_kernel' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.small_rem_kernel_unit' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.projected_remainder_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.coupling_from_unprojected' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.activity_le_ker' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.hbeta_of_steps_ker' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.steps_ker_of_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.hbeta_agrees' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.small_rem_field_of_kernel' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.chain_to_hypotheses_ker' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.chain_ker_of_chain' depends on axioms: [propext, Classical.choice, Quot.sound]
