'Insertion.sum_plus' depends on axioms: [propext, Classical.choice, Quot.sound]
'Insertion.sum_minus' depends on axioms: [propext, Classical.choice, Quot.sound]
'Insertion.mean_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Insertion.mean_rho_sigma' depends on axioms: [propext, Classical.choice, Quot.sound]
'Insertion.sector_bias_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'Bounded.single' depends on axioms: [propext, Classical.choice, Quot.sound]
'Bounded.single_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'Bounded.multi' depends on axioms: [propext, Classical.choice, Quot.sound]
'Bounded.averaged' depends on axioms: [propext, Classical.choice, Quot.sound]
'Bounded.averaged_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'SecondMoment.sqrt_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
'SecondMoment.pz_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'MultiCell.pushforward' depends on axioms: [propext, Classical.choice, Quot.sound]
'MultiCell.expand_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
'MultiCell.bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'FlipLemma.flip_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'FlipLemma.cut_formula' depends on axioms: [propext, Classical.choice, Quot.sound]
'FluxLemma.flip_le_one_sub_abs' depends on axioms: [propext, Classical.choice, Quot.sound]
'Containers.factorize' depends on axioms: [propext, Classical.choice, Quot.sound]
'Containers.container_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'FluxDuality.split' depends on axioms: [propext, Classical.choice, Quot.sound]
'FluxDuality.twisted_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'FluxDuality.bias_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'Doubling.iterate' depends on axioms: [propext, Classical.choice, Quot.sound]
'Doubling.decay' depends on axioms: [propext, Classical.choice, Quot.sound]
'ReflPos.refl_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'ReflPos.refl_cs' depends on axioms: [propext, Classical.choice, Quot.sound]
'ColumnChessboard.signed_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'ColumnChessboard.unsigned_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'ColumnChessboard.prod_expand' depends on axioms: [propext, Classical.choice, Quot.sound]
'ColumnChessboard.binomial_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'ColumnChessboard.exp_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
