'LatticeTwoColorKP.conn_erase' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.rooted_erase' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.rooted_of_connected' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.Wg_step' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.prod_mono_of_one_le' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.Wg_le' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.point_gf_le_weighted' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.prod_by_color' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.two_color_Wg_le' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.two_color_point_sum' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.two_color_root_set_sum' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.one_add_pow_le_exp' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.fix_of_exp' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.exp_one_le' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.exp_nat_le' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.lattice_fix' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.lattice_face_total' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.lattice_two_color_kp' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.sum_le_of_injOn' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.label_sum_le' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.img_spec' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.img_mem' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.img_adj' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.enc_connected' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.decode' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.enc_eq' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.thin_disjoint' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.card_le_enc' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.weight_le_G' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.encoded_sum_le' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.enc_meets_root' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.two_color_point_gf' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.two_color_root_gf' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.encoded_kp_site' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.intersect_sum_le' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.dobrushin_cond_of_kp' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.encoded_dobrushin' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.key0' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.mem_map_tF' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.mem_map_tL' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.mem_linksOf' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.mem_facesOf' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.mem_facesOf_iff' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.adj_mem_nbFF' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.mem_nbFF' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.adjF_shift' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.fl_mem' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.lf_mem' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.ll_mem' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.card_nbFF0' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.card_nbFL0' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.card_nbLF0' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.card_nbLL0' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.card_links0' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.lattice_hnb' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.filter_disjSum_left' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.filter_disjSum_right' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.lattice_hdeg' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.lattice_hfour' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.lattice_kp_site' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.lattice_dobrushin' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.blk_add' depends on axioms: [propext, Quot.sound]
'LatticeTwoColorKP.sub_blk_mem' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.box_offset' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.card_boxOff' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.box_degree' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.box_image_connected' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.box_diag' depends on axioms: [propext, choice, Quot.sound]
