'LatticeGauge.LocProjection.euler_of_homogeneous' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.marginal_of_fixed' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.schur_homogeneous' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.proj_idem' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.proj_decomp' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.loc_comm' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.comm_sub_proj' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.iterate_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.iterate_contract_ker' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.iterate_contract_remainder' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.marginal_unique' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.other_direction_drifts' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.other_direction_not_fixed' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.restrictKer_opNorm_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.exists_unique_fixed_ker' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.kkt_gauge_orthogonal' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.kkt_scale' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.kkt_homogeneous' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.pull_succ'' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.pull_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.dist_pull_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.pull_orbit' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.exists_unique_entire_orbit' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.ball_step_from_loc_A' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.window_from_loc_A' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.window_radius' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.window_numbers' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.pull_mem_sets' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.dist_pull_le_sets' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.exists_unique_entire_orbit_sets' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.isClosed_stageSet' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.window_from_loc_A_stages' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.stage_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.bounded_orbit_small' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.norm_step_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.orbit_in_small_ball' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.coupling_remainder_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.small_rem_form' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeFieldStep.rarity_chernoff' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeFieldStep.rarity_ennreal' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeFieldStep.healing_deterministic' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeFieldStep.healing_markov' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeFieldStep.kp_threshold' depends on axioms: [propext, Classical.choice, Quot.sound]
'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]
'UltravioletAssembly.window_orbit_small' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletAssembly.small_rem_field' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletAssembly.rarity_field' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletAssembly.coupling_steps_of_parts' depends on axioms: [propext, Classical.choice, Quot.sound]
