'PolymerGasDobrushin.Z_empty' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.sum_powerset_ite_forall' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.compat_insert' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.Z_insert' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.remove_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.dobrushin' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.Z_ge_exp' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.log_Z_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'KPToDobrushin.intersect_sum_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'KPToDobrushin.dobrushin_cond_of_kp' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasKP.kp_gas_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasFreeEnergy.Z_le_prod' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasFreeEnergy.abs_log_Z_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasFreeEnergy.sum_mu_le_card' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeFieldCoupling.sum_mu_le_card_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeFieldCoupling.difference_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeFieldCoupling.large_rem_from_gas' depends on axioms: [propext, Classical.choice, Quot.sound]
