'TwoColorEncoding.conn_erase' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.rooted_erase' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.rooted_of_connected' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.Wg_step' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.prod_mono_of_one_le' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.Wg_le' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.point_gf_le_weighted' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.prod_by_color' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.two_color_Wg_le' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.two_color_point_sum' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.two_color_root_set_sum' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.one_add_pow_le_exp' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.fix_of_exp' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.exp_one_le' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.exp_nat_le' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.lattice_fix' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.lattice_face_total' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.lattice_two_color_kp' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.sum_le_of_injOn' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.label_sum_le' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.img_spec' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.img_mem' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.img_adj' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.enc_connected' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.decode' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.enc_eq' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.thin_disjoint' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.card_le_enc' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.weight_le_G' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.encoded_sum_le' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.enc_meets_root' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.two_color_point_gf' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.two_color_root_gf' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.encoded_kp_site' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.intersect_sum_le' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.dobrushin_cond_of_kp' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.encoded_dobrushin' depends on axioms: [propext, choice, Quot.sound]
