'LevelConstants.w2_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'LevelConstants.w2_value' depends on axioms: [propext, Classical.choice, Quot.sound]
'LevelConstants.w2_gap' depends on axioms: [propext, Classical.choice, Quot.sound]
'LevelConstants.cubic_to_y' depends on axioms: [propext, Classical.choice, Quot.sound]
'LevelConstants.slope_of_kappa' depends on axioms: [propext, Classical.choice, Quot.sound]
'LevelConstants.slope_of_gamma' depends on axioms: [propext, Classical.choice, Quot.sound]
'LevelConstants.equal_paths' depends on axioms: [propext, Classical.choice, Quot.sound]
'LevelConstants.fine_constants' depends on axioms: [propext, Classical.choice, Quot.sound]
'LevelConstants.coarse_constants' depends on axioms: [propext, Classical.choice, Quot.sound]
'LevelConstants.threshold' depends on axioms: [propext, Classical.choice, Quot.sound]
'LevelConstants.thresholds' depends on axioms: [propext, Classical.choice, Quot.sound]
