'Lattice24KP.conn_erase' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.rooted_erase' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.rooted_of_connected' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.Wg_step' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.prod_mono_of_one_le' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.Wg_le' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.point_gf_le_weighted' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.prod_by_color' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.two_color_Wg_le' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.two_color_point_sum' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.two_color_root_set_sum' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.one_add_pow_le_exp' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.fix_of_exp' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.exp_one_le' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.exp_nat_le' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.lattice_fix' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.lattice_face_total' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.lattice_two_color_kp' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.sum_le_of_injOn' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.label_sum_le' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.img_spec' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.img_mem' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.img_adj' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.enc_connected' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.decode' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.enc_eq' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.thin_disjoint' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.card_le_enc' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.weight_le_G' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.encoded_sum_le' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.enc_meets_root' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.two_color_point_gf' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.two_color_root_gf' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.encoded_kp_site' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.intersect_sum_le' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.dobrushin_cond_of_kp' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.encoded_dobrushin' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.key0' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.mem_map_tF' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.mem_map_tL' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.mem_linksOf' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.mem_facesOf' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.mem_facesOf_iff' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.adj_mem_nbFF' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.mem_nbFF' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.adjF_shift' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.fl_mem' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.lf_mem' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.ll_mem' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.card_links0' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.adj24_mem' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.adj24_shift' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.mem_nbFF24' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.fl24_mem' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.lf24_mem' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.ll24_mem' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.card_nbFF24_0' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.card_nbFL24_0' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.card_nbLF24_0' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.card_nbLL24_0' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.lattice24_hnb' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.filter_disjSum_left' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.filter_disjSum_right' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.lattice24_hdeg' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.lattice_hfour' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.lattice24_fix' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.lattice24_face_total' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.encoded_kp_site24' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.lattice_kp_site24' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.quad_le_pow' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.exp_two_gt' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.face24_fails' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.face24_holds_685' depends on axioms: [propext, choice, Quot.sound]
