'BoxTwoColorKP.conn_erase' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.rooted_erase' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.rooted_of_connected' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.Wg_step' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.prod_mono_of_one_le' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.Wg_le' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.point_gf_le_weighted' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.prod_by_color' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.two_color_Wg_le' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.two_color_point_sum' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.two_color_root_set_sum' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.one_add_pow_le_exp' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.fix_of_exp' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.exp_one_le' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.exp_nat_le' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.lattice_fix' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.lattice_face_total' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.lattice_two_color_kp' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.sum_le_of_injOn' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.label_sum_le' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.img_spec' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.img_mem' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.img_adj' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.enc_connected' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.decode' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.enc_eq' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.thin_disjoint' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.card_le_enc' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.weight_le_G' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.encoded_sum_le' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.enc_meets_root' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.two_color_point_gf' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.two_color_root_gf' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.encoded_kp_site' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.intersect_sum_le' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.dobrushin_cond_of_kp' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.encoded_dobrushin' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.key0' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.mem_map_tF' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.mem_map_tL' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.mem_linksOf' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.mem_facesOf' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.mem_facesOf_iff' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.adj_mem_nbFF' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.mem_nbFF' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.adjF_shift' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.fl_mem' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.lf_mem' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.ll_mem' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.blk_add' depends on axioms: [propext, Quot.sound]
'BoxTwoColorKP.sub_blk_mem' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.off_mem' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.card_offFF' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.card_cube81' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.nbFL0_bdd' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.nbLF0_bdd' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.nbLL0_bdd' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.blk_sub_mem_cube' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.card_offc' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.box_hnb' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.box_hdeg' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.bimg_adj' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.bimg_connected' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.box_fix' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.box_kp_site' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.quad_le_pow' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.exp_two_gt' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.box_fails' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.box_holds_761' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.box_hsite' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.box_dobrushin' depends on axioms: [propext, choice, Quot.sound]
