'LargeSetRegulator.full_blocks_card' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeSetRegulator.image_card_regulated' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeSetRegulator.image_card_fraction' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeSetRegulator.size_condition_regulated' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeSetRegulator.weight_preserving_contraction' depends on axioms: [propext, Classical.choice, Quot.sound]
