'CacheCeilingAttained.keepAll_demand' depends on axioms: [propext]
'CacheCeilingAttained.countNewAux_congr' depends on axioms: [propext, Quot.sound]
'CacheCeilingAttained.keepAll_attains_wall' depends on axioms: [propext, Classical.choice, Quot.sound]
'CacheCeilingAttained.keepAll_hits_eq_wall' depends on axioms: [propext, Classical.choice, Quot.sound]