'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]
'MarginRatioTwo.half_b2_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.half_b2_upper' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.ball_bound_value' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.ball_c022' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.ball_c04_fails_beta28' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.ball_c04' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_beta28_c022' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_c04_fform_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_ker_beta28_c022' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_ker_beta54_c04' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_ker_beta40_c04_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginNumbers.bRatioTwo_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginNumbers.C2_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginNumbers.margin_beta28' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginNumbers.margin_beta54' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginNumbers.steps_beta28' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginNumbers.hbeta_beta28' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginWindow.margin_beta33' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginWindow.margin_beta36' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginWindow.margin_beta38' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginWindow.c04_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginWindow.c04_ball_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginWindow.c022_ball' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginWindow.steps_window' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginWindow.hbeta_beta33' depends on axioms: [propext, Classical.choice, Quot.sound]
