'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]
