'PolymerBlocking.recount_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerBlocking.blocking_kp' depends on axioms: [propext, Classical.choice, Quot.sound]
