'LatticeGaugeTailTypeClassification.flat_weighted_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeTailTypeClassification.flat_weighted_unbounded' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeTailTypeClassification.exp_weighted_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeTailTypeClassification.power_sum_uniform' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeTailTypeClassification.power_sum_unbounded' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeTailTypeClassification.power_sum_unbounded_borderline' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
