'BoxConnectivity.dist_sum_step' depends on axioms: [propext, Classical.choice, Quot.sound]
'BoxConnectivity.step_inBox' depends on axioms: [propext, Classical.choice, Quot.sound]
'BoxConnectivity.step_edge' depends on axioms: [propext, Classical.choice, Quot.sound]
'BoxConnectivity.exists_boundary_edge' depends on axioms: [propext, Classical.choice, Quot.sound]
'BoxConnectivity.block_is_box' depends on axioms: [propext, Classical.choice, Quot.sound]
