'shift_index' depends on axioms: [propext, Classical.choice, Quot.sound]
'shift_index' depends on axioms: [propext, Classical.choice, Quot.sound]
'bshift_index' depends on axioms: [propext, Classical.choice, Quot.sound]
'bshift_comp_shift' depends on axioms: [propext, Classical.choice, Quot.sound]