'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]
