'WeakUltravioletExistence.exists_bare_inverse_coupling' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.exists_subseq_tendsto_probabilityMeasure' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'WeakUltravioletExistence.exists_common_subseq' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.limit_consistent' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.reflection_positivity_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.approx_invariance_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.closed_mass_lower_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.exists_subseq_tendsto_on_countable' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.continuous_extension_of_tendsto' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.exists_subseq_continuous_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.invariance_of_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.quadratic_positivity_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.invariance_extends_by_density' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.tendsto_of_summable_increments' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.subseq_limit_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.weak_uv_block_skeleton' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.weak_uv_observable_skeleton' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.weak_uv_observable_full' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.weak_uv_skeleton' depends on axioms: [propext, Classical.choice, Quot.sound]
'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]
'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]
'ChainEndToEnd.chain_end_to_end' depends on axioms: [propext, Classical.choice, Quot.sound]
'ChainEndToEnd.chain_ker_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]
'FineSupportReflection.dependsOn_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'FineSupportReflection.coarse_rp_of_fine_support' depends on axioms: [propext, Classical.choice, Quot.sound]
'FineSupportReflection.integrable_of_bdd' depends on axioms: [propext, Classical.choice, Quot.sound]
'FineSupportReflection.matrix_rp_of_fine_support' depends on axioms: [propext, Classical.choice, Quot.sound]
'FineSupportReflection.reflection_positive_of_fine' depends on axioms: [propext, Classical.choice, Quot.sound]
'FineSupportReflection.positivity_of_fine' depends on axioms: [propext, Classical.choice, Quot.sound]
'FineSupportReflection.chain_end_to_end_fine_support' depends on axioms: [propext, Classical.choice, Quot.sound]
