'PolymerMerge.intersect_sum_le'' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerMerge.one_side_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerMerge.merge_pairs_le' depends on axioms: [propext, Classical.choice, Quot.sound]
