'IndexTwoWays.card_monomials' depends on axioms: [propext, Classical.choice, Quot.sound]
'IndexTwoWays.choose_zero_between' depends on axioms: [propext, Quot.sound]
'IndexTwoWays.P1_count' depends on axioms: [propext, Classical.choice, Quot.sound]