'BoundaryRegulator.image_card_boundary' depends on axioms: [propext, Classical.choice, Quot.sound]
'BoundaryRegulator.image_card_boundary_real' depends on axioms: [propext, Classical.choice, Quot.sound]
'BoundaryRegulator.size_condition_boundary' depends on axioms: [propext, Classical.choice, Quot.sound]
