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