'TwoColorPolymerSum.conn_erase' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.rooted_erase' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.rooted_of_connected' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.Wg_step' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.prod_mono_of_one_le' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.Wg_le' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.point_gf_le_weighted' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.prod_by_color' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.two_color_Wg_le' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.two_color_point_sum' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.two_color_root_set_sum' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.one_add_pow_le_exp' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.fix_of_exp' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.exp_one_le' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.exp_nat_le' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.lattice_fix' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.lattice_face_total' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.lattice_two_color_kp' depends on axioms: [propext, choice, Quot.sound]
