'InfinityMinusInfinity.zois_theorem1' depends on axioms: [propext, Classical.choice, Quot.sound]
'InfinityMinusInfinity.endo_index_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'InfinityMinusInfinity.shift_index_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'InfinityMinusInfinity.bshift_index_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'InfinityMinusInfinity.bshift_shift_index' depends on axioms: [propext, Classical.choice, Quot.sound]
'InfinityMinusInfinity.shift_bshift_index' depends on axioms: [propext, Classical.choice, Quot.sound]
'InfinityMinusInfinity.shift_bshift_ne_id' depends on axioms: [propext, Classical.choice, Quot.sound]