'GibbsContinuity.continuous_weighted_integral' depends on axioms: [propext, Classical.choice, Quot.sound]
'GibbsContinuity.partition_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'GibbsContinuity.continuous_gibbs_expectation' depends on axioms: [propext, Classical.choice, Quot.sound]
'GibbsContinuity.continuousOn_effective_coupling' depends on axioms: [propext, Classical.choice, Quot.sound]
'GibbsContinuity.continuous_expectation_vector' depends on axioms: [propext, Classical.choice, Quot.sound]
