== ConnectedSetCounting.lean 'ConnectedSetCounting.conn_erase' depends on axioms: [propext, choice, Quot.sound] 'ConnectedSetCounting.rooted_erase' depends on axioms: [propext, choice, Quot.sound] 'ConnectedSetCounting.W_step' depends on axioms: [propext, choice, Quot.sound] 'ConnectedSetCounting.W_le' depends on axioms: [propext, choice, Quot.sound] 'ConnectedSetCounting.rooted_of_connected' depends on axioms: [propext, choice, Quot.sound] 'ConnectedSetCounting.connected_gf_le' depends on axioms: [propext, choice, Quot.sound] 'ConnectedSetCounting.one_add_inv_pow_le' depends on axioms: [propext, choice, Quot.sound] 'ConnectedSetCounting.connected_count_le' depends on axioms: [propext, choice, Quot.sound] 'ConnectedSetCounting.connected_count_real' depends on axioms: [propext, choice, Quot.sound] 'ConnectedSetCounting.connectedSetCount_of_bounded' depends on axioms: [propext, choice, Quot.sound] 'ConnectedSetCounting.countingFromDegree_of_exists' depends on axioms: [propext, choice, Quot.sound] 'ConnectedSetCounting.connectedSetCount_fails_at_zero' depends on axioms: [propext, choice, Quot.sound] 'ConnectedSetCounting.point_gf_le' depends on axioms: [propext, choice, Quot.sound] 'ConnectedSetCounting.point_kp_sum_le' depends on axioms: [propext, choice, Quot.sound] == TwoColorPolymerSum.lean '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] == KPToDobrushin.lean 'KPToDobrushin.intersect_sum_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'KPToDobrushin.dobrushin_cond_of_kp' depends on axioms: [propext, Classical.choice, Quot.sound] == TwoColorEncoding.lean '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] == LatticeTwoColorKP.lean '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] == BoxTwoColorKP.lean '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] == Lattice24KP.lean '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] == BoxFromFace.lean 'BoxFromFace.conn_erase' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.rooted_erase' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.rooted_of_connected' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.Wg_step' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.prod_mono_of_one_le' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.Wg_le' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.point_gf_le_weighted' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.prod_by_color' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.two_color_Wg_le' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.two_color_point_sum' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.two_color_root_set_sum' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.one_add_pow_le_exp' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.fix_of_exp' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.exp_one_le' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.exp_nat_le' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.lattice_fix' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.lattice_face_total' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.lattice_two_color_kp' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.sum_le_of_injOn' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.label_sum_le' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.img_spec' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.img_mem' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.img_adj' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.enc_connected' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.decode' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.enc_eq' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.thin_disjoint' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.card_le_enc' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.weight_le_G' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.encoded_sum_le' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.enc_meets_root' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.two_color_point_gf' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.two_color_root_gf' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.encoded_kp_site' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.intersect_sum_le' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.dobrushin_cond_of_kp' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.encoded_dobrushin' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.key0' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.mem_map_tF' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.mem_map_tL' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.mem_linksOf' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.mem_facesOf' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.mem_facesOf_iff' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.adj_mem_nbFF' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.mem_nbFF' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.adjF_shift' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.fl_mem' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.lf_mem' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.ll_mem' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.blk_add' depends on axioms: [propext, Quot.sound] 'BoxFromFace.sub_blk_mem' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.off_mem' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.card_offFF' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.card_cube81' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.nbFL0_bdd' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.nbLF0_bdd' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.nbLL0_bdd' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.blk_sub_mem_cube' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.card_offc' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.box_hnb' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.box_hdeg' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.bimg_adj' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.bimg_connected' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.box_fix' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.box_kp_site' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.quad_le_pow' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.exp_two_gt' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.box_fails' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.box_holds_761' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.box_hsite' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.box_dobrushin' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.weight_le_Gc' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.encoded_sum_le_c' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.fiber_box_le' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.card_corners' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.card_boxFaces' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.card_boxLinks' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.cell_thin_sub' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.cell_def_sub' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.cell_prod_le' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.box_hz_from_face' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.epsBox_numbers' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.box_hsite_eq_face_sum' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.box_hsite_of_face_sum' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.face_to_box_dobrushin' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.card_nbFF0' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.card_nbFL0' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.card_nbLF0' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.card_nbLL0' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.card_links0' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.lattice_hnb' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.filter_disjSum_left' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.filter_disjSum_right' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.lattice_hdeg' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.lattice_hfour' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.card_boxRoot_links' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.enc_meets_boxRoot' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.box_event_bridge' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.bridge_numbers_gamma' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.bridge_numbers_chernoff' depends on axioms: [propext, choice, Quot.sound] == PolymerGasDobrushin.lean 'PolymerGasDobrushin.Z_empty' depends on axioms: [propext, Classical.choice, Quot.sound] 'PolymerGasDobrushin.sum_powerset_ite_forall' depends on axioms: [propext, Classical.choice, Quot.sound] 'PolymerGasDobrushin.compat_insert' depends on axioms: [propext, Classical.choice, Quot.sound] 'PolymerGasDobrushin.Z_insert' depends on axioms: [propext, Classical.choice, Quot.sound] 'PolymerGasDobrushin.remove_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'PolymerGasDobrushin.dobrushin' depends on axioms: [propext, Classical.choice, Quot.sound] 'PolymerGasDobrushin.Z_ge_exp' depends on axioms: [propext, Classical.choice, Quot.sound] 'PolymerGasDobrushin.log_Z_ge' depends on axioms: [propext, Classical.choice, Quot.sound] == ClassSiteSum.lean 'ClassSiteSum.site_sum_le_class_sum' depends on axioms: [propext, Classical.choice, Quot.sound] 'ClassSiteSum.hsite_of_class_sum' depends on axioms: [propext, Classical.choice, Quot.sound] 'ClassSiteSum.single_class_sum' depends on axioms: [propext, Classical.choice, Quot.sound] 'ClassSiteSum.tail_le_of_ratio' depends on axioms: [propext, Classical.choice, Quot.sound] == SizeSplitKP.lean 'SizeSplitKP.sum_split_by_card' depends on axioms: [propext, Classical.choice, Quot.sound] 'SizeSplitKP.fat_sum_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'SizeSplitKP.geometric_tail_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'SizeSplitKP.size_split_site_sum' depends on axioms: [propext, Classical.choice, Quot.sound] 'SizeSplitKP.fat_condition_iff' depends on axioms: [propext, Classical.choice, Quot.sound] 'SizeSplitKP.allowed_eps_scale' depends on axioms: [propext, Classical.choice, Quot.sound] == BoxConnectivity.lean 'BoxConnectivity.dist_sum_step' depends on axioms: [propext, Classical.choice, Quot.sound] 'BoxConnectivity.step_inBox' depends on axioms: [propext, Classical.choice, Quot.sound] 'BoxConnectivity.step_edge' depends on axioms: [propext, Classical.choice, Quot.sound] 'BoxConnectivity.exists_boundary_edge' depends on axioms: [propext, Classical.choice, Quot.sound] 'BoxConnectivity.block_is_box' depends on axioms: [propext, Classical.choice, Quot.sound] == BoxGasFromFaceSum.lean 'BoxFromFace.conn_erase' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.rooted_erase' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.rooted_of_connected' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.Wg_step' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.prod_mono_of_one_le' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.Wg_le' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.point_gf_le_weighted' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.prod_by_color' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.two_color_Wg_le' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.two_color_point_sum' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.two_color_root_set_sum' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.one_add_pow_le_exp' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.fix_of_exp' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.exp_one_le' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.exp_nat_le' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.lattice_fix' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.lattice_face_total' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.lattice_two_color_kp' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.sum_le_of_injOn' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.label_sum_le' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.img_spec' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.img_mem' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.img_adj' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.enc_connected' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.decode' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.enc_eq' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.thin_disjoint' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.card_le_enc' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.weight_le_G' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.encoded_sum_le' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.enc_meets_root' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.two_color_point_gf' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.two_color_root_gf' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.encoded_kp_site' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.intersect_sum_le' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.dobrushin_cond_of_kp' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.encoded_dobrushin' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.key0' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.mem_map_tF' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.mem_map_tL' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.mem_linksOf' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.mem_facesOf' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.mem_facesOf_iff' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.adj_mem_nbFF' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.mem_nbFF' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.adjF_shift' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.fl_mem' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.lf_mem' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.ll_mem' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.blk_add' depends on axioms: [propext, Quot.sound] 'BoxFromFace.sub_blk_mem' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.off_mem' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.card_offFF' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.card_cube81' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.nbFL0_bdd' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.nbLF0_bdd' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.nbLL0_bdd' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.blk_sub_mem_cube' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.card_offc' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.box_hnb' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.box_hdeg' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.bimg_adj' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.bimg_connected' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.box_fix' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.box_kp_site' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.quad_le_pow' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.exp_two_gt' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.box_fails' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.box_holds_761' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.box_hsite' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.box_dobrushin' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.weight_le_Gc' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.encoded_sum_le_c' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.fiber_box_le' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.card_corners' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.card_boxFaces' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.card_boxLinks' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.cell_thin_sub' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.cell_def_sub' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.cell_prod_le' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.box_hz_from_face' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.epsBox_numbers' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.box_hsite_eq_face_sum' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.box_hsite_of_face_sum' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.face_to_box_dobrushin' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.card_nbFF0' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.card_nbFL0' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.card_nbLF0' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.card_nbLL0' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.card_links0' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.lattice_hnb' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.filter_disjSum_left' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.filter_disjSum_right' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.lattice_hdeg' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.lattice_hfour' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.card_boxRoot_links' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.enc_meets_boxRoot' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.box_event_bridge' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.bridge_numbers_gamma' depends on axioms: [propext, choice, Quot.sound] 'BoxFromFace.bridge_numbers_chernoff' depends on axioms: [propext, choice, Quot.sound] 'PolymerGasDobrushin.Z_empty' depends on axioms: [propext, Classical.choice, Quot.sound] 'PolymerGasDobrushin.sum_powerset_ite_forall' depends on axioms: [propext, Classical.choice, Quot.sound] 'PolymerGasDobrushin.compat_insert' depends on axioms: [propext, Classical.choice, Quot.sound] 'PolymerGasDobrushin.Z_insert' depends on axioms: [propext, Classical.choice, Quot.sound] 'PolymerGasDobrushin.remove_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'PolymerGasDobrushin.dobrushin' depends on axioms: [propext, Classical.choice, Quot.sound] 'PolymerGasDobrushin.Z_ge_exp' depends on axioms: [propext, Classical.choice, Quot.sound] 'PolymerGasDobrushin.log_Z_ge' depends on axioms: [propext, Classical.choice, Quot.sound] 'BoxGasFromFaceSum.boxInc_symm' depends on axioms: [propext, Classical.choice, Quot.sound] 'BoxGasFromFaceSum.boxA_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound] 'BoxGasFromFaceSum.box_dobrushin_of_face_sum' depends on axioms: [propext, Classical.choice, Quot.sound] 'BoxGasFromFaceSum.box_gas_partition_of_face_sum' depends on axioms: [propext, Classical.choice, Quot.sound]