'CrossUnits.adjacent_no_anchored_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'CrossUnits.one_no_anchored_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'CornerCertificate.four_alpha_local' depends on axioms: [propext, Classical.choice, Quot.sound]
'CornerCertificate.four_beta_local' depends on axioms: [propext, Classical.choice, Quot.sound]
'CornerCertificate.four_gamma_local' depends on axioms: [propext, Classical.choice, Quot.sound]
'CornerCertificate.four_betaTranspose_local' depends on axioms: [propext, Classical.choice, Quot.sound]
'CornerCertificate.four_gammaTranspose_local' depends on axioms: [propext, Classical.choice, Quot.sound]
'CornerCertificate.four_local' depends on axioms: [propext, Classical.choice, Quot.sound]
'CornerCertificate.five_alpha_local' depends on axioms: [propext, Classical.choice, Quot.sound]
'CornerCertificate.five_beta_local' depends on axioms: [propext, Classical.choice, Quot.sound]
'CornerCertificate.five_gamma_local' depends on axioms: [propext, Classical.choice, Quot.sound]
'CornerCertificate.five_betaTranspose_local' depends on axioms: [propext, Classical.choice, Quot.sound]
'CornerCertificate.five_gammaTranspose_local' depends on axioms: [propext, Classical.choice, Quot.sound]
'CornerCertificate.five_local' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.HalfStripObstruction.no_half_strip' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.rectangle_implies_half_strip' depends on axioms: [propext, Classical.choice, Quot.sound]
'PositiveConstructions.strip_tiles' depends on axioms: [propext, Classical.choice, Quot.sound]
'PositiveConstructions.bent_tiles' depends on axioms: [propext, Classical.choice, Quot.sound]
'PositiveConstructions.strip_tileable' depends on axioms: [propext, Classical.choice, Quot.sound]
'PositiveConstructions.bent_tileable' depends on axioms: [propext, Classical.choice, Quot.sound]
'PositiveHierarchy.strip_tiles_halfplane' depends on axioms: [propext, Classical.choice, Quot.sound]
'PositiveHierarchy.strip_tiles_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'PositiveHierarchy.bent_tiles_quadrant' depends on axioms: [propext, Classical.choice, Quot.sound]
'PositiveHierarchy.quadrant_tiles_halfplane' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.RepObstruction.no_lattice_rep_of_replay' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.RepObstruction.no_small_target' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.RepObstruction.no_target_of_replay' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.RepObstruction.no_large_target_of_replay' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.RepObstruction.no_bounded_progress' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.RepObstruction.no_small_scale_of_composition' depends on axioms: [propext, Quot.sound]
'PolyominoFormal.RepObstruction.wall_buffer' depends on axioms: [propext, Quot.sound]
'PolyominoFormal.RepObstruction.selected_tile_below_top' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.RepObstruction.supported_query_in_target' depends on axioms: [propext, Quot.sound]
'PolyominoFormal.normalize_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.CoreBoundaryObstructions.positive_cross_no_halfplane' depends on axioms: [propext,
'PolyominoFormal.CoreBoundaryObstructions.positive_cross_no_scaled_copy' depends on axioms: [propext,
'PolyominoFormal.rectangle_implies_rep' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.no_rep_of_replay' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.p4_exact_bs' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.p5_exact_bs' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.ElementaryRectangles.bar_rectangle_tileable' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.ElementaryRectangles.unit_l_rectangle_tileable' depends on axioms: [propext,
'PolyominoFormal.SmallTRectangles.t1_rectangle_tileable' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.SmallTRectangles.t2_rectangle_tileable' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.SmallTRectangles.t3_rectangle_tileable' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.exact_rectangle_of_rectangle' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.p3_exact_rectangle' depends on axioms: [propext, Classical.choice, Quot.sound]
'TPlane.two_short_no_anchored_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'CornerCertificate.affine_alpha_local' depends on axioms: [propext, Classical.choice, Quot.sound]
'CornerCertificate.affine_beta_local' depends on axioms: [propext, Classical.choice, Quot.sound]
'CornerCertificate.affine_gamma_local' depends on axioms: [propext, Classical.choice, Quot.sound]
'CornerCertificate.affine_betaTranspose_local' depends on axioms: [propext, Classical.choice, Quot.sound]
'CornerCertificate.affine_gammaTranspose_local' depends on axioms: [propext, Classical.choice, Quot.sound]
'CornerCertificate.large_local' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.classify_gun' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.gun_half_strip_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.gun_rep_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.TBoundary.no_quadrant' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.TRepObstruction.no_rep' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.unit_stem_exact_strip' depends on axioms: [propext, Classical.choice, Quot.sound]
'PositivePlaneUnit.tiles_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'PositivePlaneTwo.tiles_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'PositivePlaneExceptional.tiles_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'PositiveCross.tiles_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.adjacent_units_no_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.one_unit_no_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.short_stem_two_arm_no_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LongCrossObstruction.anchored_no_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LongCrossObstruction.all_long_no_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.CrossClassification.plane_requires_opposite_units' depends on axioms: [propext,
'PositiveTheorems.t_plane_of_conditions' depends on axioms: [propext, Classical.choice, Quot.sound]
'PositiveTheorems.cross_plane_of_opposite_units' depends on axioms: [propext, Classical.choice, Quot.sound]
'PositiveTheorems.cross_plane_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'PositiveTheorems.t_two_units_positive_profile' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.classify_positive_cross' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.rep_arbitrarily_large' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.same_copies_rep' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.TilingCompactness.compact' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.TilingCompactness.world_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.rep_zero_south_implies_quadrant' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.gun_classified' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.positive_cross_classified' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.Q_equal_no_quadrant' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.Q_equal_bounded_obstruction' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.Q_fixed_3_2_no_quadrant' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.Q_fixed_3_2_bounded_obstruction' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.Q_fixed_4_2_no_quadrant' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.Q_fixed_4_2_bounded_obstruction' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.Q_fixed_4_3_no_quadrant' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.Q_fixed_4_3_bounded_obstruction' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.b_two_small_no_quadrant' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.no_quadrant_4_3' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.HP_equal_tip_long_no_shifted_anchor' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.HP_equal_tip_long_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_unequal_tip_short_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_unequal_tip_short_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_shortlong_tip_short_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_shortlong_tip_short_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRegion.equal_avoid_tips' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.unequal_avoid_short_tips' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.shortlong_avoid_short_tips' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.shortlong_quadrant_avoid_short_tips' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.HP_shortlong_tip_long_pruned_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_shortlong_tip_long_pruned_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRegion.Q_shortlong_anchored_anchored_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRegion.Q_shortlong_anchored_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRegion.shortlong_origin_junction' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.shortlong_no_quadrant' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.THalfPlaneStarters.short_run_forms' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.THalfPlaneStarters.blocked_short_run' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.THalfPlaneStarters.boundary_forms' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.THalfPlaneStarters.no_three_starters' depends on axioms: [propext, Quot.sound]
'PolyominoFormal.THalfPlaneGaps.no_short_horizontal_pair' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.THalfPlaneGaps.all_horizontal_short_impossible' depends on axioms: [propext,
'PolyominoFormal.LHalfPlaneEqual.blocked_short_run' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.HP_equal_bar_long_fixed_3_pruned_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_equal_bar_long_fixed_3_pruned_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_equal_bar_long_fixed_4_pruned_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_equal_bar_long_fixed_4_pruned_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_equal_bar_long_fixed_5_pruned_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_equal_bar_long_fixed_5_pruned_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRegion.equal_finite_no_half_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.THalfPlaneDeepGaps.blocked_deep_run' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.THalfPlaneDeepGaps.all_horizontal_long_impossible' depends on axioms: [propext,
'PolyominoFormal.THalfPlane.no_s_right' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.THalfPlane.right_v_neighbor_horizontal' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.THalfPlane.no_right_v_two' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.THalfPlane.no_halfplane_two_short' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.THalfPlane.no_halfplane_two' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.THalfPlane.no_halfplane_unit_long' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LHalfPlaneEqual.no_halfplane_large' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LHalfPlaneEqual.no_halfplane' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.PositiveLPlane.tiles_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.PositiveLStrip.strip_tileable' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.PositiveLSpecial.strip_tileable' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.sorted_L_classified_of_obstructions' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.sorted_L_classified_of_unequal' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.HP_boundary_unequal_tip_long_pruned_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_boundary_unequal_tip_long_pruned_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRegion.unequal_avoid_boundary_tips' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.HP_samebars_unequal_bar_long_pruned_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_samebars_unequal_bar_long_pruned_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRegion.same_long_bars_impossible' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.same_long_bars_left_impossible' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.avoid_same_boundary_bars' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.HP_boundaryall_unequal_corner_long_pruned_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_boundaryall_unequal_corner_long_pruned_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRegion.long_corner_right_impossible' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.avoid_long_boundary_corner' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LHalfPlaneAlternating.local_short_tip_node000' depends on axioms: [propext,
'PolyominoFormal.LHalfPlaneAlternating.local_long_tip_node000' depends on axioms: [propext,
'PolyominoFormal.LHalfPlaneLocal.enclosed_thin_rectangle' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LHalfPlaneLocal.run_forms' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LHalfPlaneLocal.blocked_short_tall_run' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LHalfPlaneAlternating.no_right_short_starter' depends on axioms: [propext,
'PolyominoFormal.LHalfPlaneAlternating.no_left_short_starter' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LHalfPlaneAlternating.no_right_long_starter' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LHalfPlaneAlternating.early_horizontal' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LHalfPlaneAlternating.no_left_long_starter' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LHalfPlaneAlternating.no_same_short_bars' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LHalfPlaneAlternating.no_left_long_starter_extended' depends on axioms: [propext,
'PolyominoFormal.LHalfPlaneAlternating.no_short_starter' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LHalfPlaneAlternating.no_near_left_long_starter_strong' depends on axioms: [propext,
'PolyominoFormal.LHalfPlaneAlternating.no_short_starter_three_pockets' depends on axioms: [propext,
'PolyominoFormal.LHalfPlaneAlternating.no_right_long_starter_eight' depends on axioms: [propext,
'PolyominoFormal.LHalfPlaneAlternating.no_left_long_starter_eight' depends on axioms: [propext,
'PolyominoFormal.LRegion.avoid_boundary_pairs' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.HP_unequal_outward_long_pruned_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_unequal_outward_long_pruned_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRegion.outward_long_corner_right_impossible' depends on axioms: [propext,
'PolyominoFormal.LRegion.avoid_outward_long_boundary_corner' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LHalfPlaneAlternating.row_one_horizontal' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LHalfPlaneAlternating.first_horizontal_bar' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LStarterRuns.no_five_starters' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LStarterRuns.blocked_short_run' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LStarterRuns.no_four_starters_with_right_wall' depends on axioms: [propext,
'PolyominoFormal.LStarterRuns.blocked_short_run_one_tall' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LHalfPlaneAlternating.first_two_bars' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LHalfPlaneAlternating.no_left_junction_after_short' depends on axioms: [propext,
'PolyominoFormal.LHalfPlaneAlternating.no_first_short_away' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LHalfPlaneAlternating.successor_horizontal' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LHalfPlaneAlternating.long_bar_unique' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LHalfPlaneAlternating.two_bar_count' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.HP_unequal_first_short_away_bthree_pruned_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_unequal_first_short_away_bthree_pruned_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_alternating_unequal_bar_long_fixed_5_3_pruned_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_alternating_unequal_bar_long_fixed_5_3_pruned_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_unequal_bar_short_fixed_5_3_pruned_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_unequal_bar_short_fixed_5_3_pruned_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LHalfPlaneAssembly.no_halfplane_from_boundary' depends on axioms: [propext,
'PolyominoFormal.LHalfPlaneAssembly.no_halfplane_from_eight' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LHalfPlaneFiveThree.no_halfplane' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.HP_unequal_after_short_left_bthree_pruned_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_unequal_after_short_left_bthree_pruned_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LHalfPlaneAlternating.first_two_bars_all' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LHalfPlaneAlternating.no_left_junction_after_first_short' depends on axioms: [propext,
'PolyominoFormal.LHalfPlaneAlternating.no_first_short_away_all' depends on axioms: [propext,
'PolyominoFormal.LHalfPlaneAlternating.left_long_pattern_of_no_outer' depends on axioms: [propext,
'PolyominoFormal.LHalfPlaneAlternating.endpoint_patterns_force_delta_two' depends on axioms: [propext,
'PolyominoFormal.LHalfPlaneAlternating.mixed_motif_of_delta_two' depends on axioms: [propext,
'PolyominoFormal.LHalfPlaneAlternating.delta_two_of_outer_obstruction' depends on axioms: [propext,
'PolyominoFormal.LHalfPlaneUnequal.no_eight_of_delta_and_mixed' depends on axioms: [propext,
'PolyominoFormal.LHalfPlaneUnequal.no_halfplane_from_inputs' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LHalfPlaneShortbarAssembly.inner_forms' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LHalfPlaneShortbarAssembly.no_shortbar_from_seven' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_boundaryall_unequal_bar_short_check_pruned_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_boundaryall_unequal_bar_short_check_pruned_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_boundaryall_unequal_shortbar_west_short_pruned_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_boundaryall_unequal_shortbar_west_short_pruned_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_boundaryall_unequal_shortbar_tip_right_pruned_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_boundaryall_unequal_shortbar_tip_right_pruned_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LHalfPlaneShortbarAssembly.long_tip_right' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LHalfPlaneShortbarAssembly.upright_short_left' depends on axioms: [propext,
'PolyominoFormal.LHalfPlaneShortbarAssembly.short_tip_right' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.HP_adjacent_bar_short_branch_pruned_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_adjacent_bar_short_branch_pruned_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_separated_bar_short_branch_pruned_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_separated_bar_short_branch_pruned_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRegion.upright_long_shortbar_obstruction' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.avoid_short_upright_long' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.HP_boundaryall_adjacent_hwest_local_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_boundaryall_adjacent_hwest_local_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_boundaryall_delta_two_hwest_local_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_boundaryall_delta_two_hwest_local_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LHalfPlaneShortbarAssembly.upright_long_left_near' depends on axioms: [propext,
'PolyominoFormal.LShortRuns.blocked_run_both_caps' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LShortRuns.blocked_two_run' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRunCertificates.tiling_extended_run_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRunCertificates.tiling_extended_down_run_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRunCertificates.tiling_extended_right_run_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRunCertificates.tiling_extended_left_run_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRunCertificates.tiling_run_obstruction' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRunCertificates.tiling_down_run_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRunCertificates.tiling_right_run_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRunCertificates.tiling_left_run_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRegion.same_short_bars_right_impossible' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.avoid_same_short_bars' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.HP_boundaryall_separated_hwest_away_pruned_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_boundaryall_separated_hwest_away_pruned_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LHalfPlaneShortbarAssembly.upright_long_left' depends on axioms: [propext,
'PolyominoFormal.LHalfPlaneShortbarAssembly.left_neighbor_forms' depends on axioms: [propext,
'PolyominoFormal.LHalfPlaneShortbarAssembly.no_shortbar_from_six_and_neighbors' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_boundaryall_unequal_vleft_longneighbor_pruned_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_boundaryall_unequal_vleft_longneighbor_pruned_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_boundaryall_unequal_vleft_eastneighbor_pruned_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_boundaryall_unequal_vleft_eastneighbor_pruned_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LHalfPlaneShortbarAssembly.west_long_neighbor' depends on axioms: [propext,
'PolyominoFormal.LHalfPlaneShortbarAssembly.east_long_neighbor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_unequal_nested_short_delta_one_pruned_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_unequal_nested_short_delta_one_pruned_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_optimized_unequal_nested_short_bfour_delta_two_pruned_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_optimized_unequal_nested_short_bfour_delta_two_pruned_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_optimized_unequal_nested_short_bfive_delta_two_pruned_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_optimized_unequal_nested_short_bfive_delta_two_pruned_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_optimized_unequal_nested_short_bge6_delta_two_pruned_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_optimized_unequal_nested_short_bge6_delta_two_pruned_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRegion.nested_short_near_obstruction' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.HP_separated_front_short_window_pruned_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_separated_front_short_window_pruned_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRegion.short_window_upright_long_impossible' depends on axioms: [propext,
'PolyominoFormal.LRegion.short_window_upright_long_shifted' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.tiling_reflected_window_obstruction' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.tiling_short_window_obstruction' depends on axioms: [propext, Classical.choice, Quot.sound]
'LRegionArithmetic.HP_unequal_nested_short_delta_ge_three_pruned_n745_run_tall' depends on axioms: [propext, Quot.sound]
'LRegionArithmetic.HP_unequal_nested_short_delta_ge_three_pruned_n887_run_floor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_unequal_nested_short_delta_ge_three_pruned_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_unequal_nested_short_delta_ge_three_pruned_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRegion.nested_short_large_obstruction' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LHalfPlaneShortbarAssembly.nested_short' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LHalfPlaneShortbarAssembly.no_shortbars' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.HP_adjacent_outer_short_pair_pruned_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_adjacent_outer_short_pair_pruned_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_separated_outer_short_pair_away_pruned_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_separated_outer_short_pair_away_pruned_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LHalfPlaneAlternating.outer_pair_away_impossible' depends on axioms: [propext,
'PolyominoFormal.LHalfPlaneAlternating.delta_two' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LRegion.HP_optimized_unequal_mixed_nonexception_delta_two_pruned_no_shifted_anchor' depends on axioms: [propext,
'PolyominoFormal.LRegion.HP_optimized_unequal_mixed_nonexception_delta_two_pruned_bounded_obstruction' depends on axioms: [propext,
'PolyominoFormal.LHalfPlaneMixedMotif.mixed_impossible' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.LHalfPlaneUnequal.no_halfplane' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.THalfPlaneUnit.no_short_v_origin' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.THalfPlaneUnit.horizontal_cover_unit' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.THalfPlaneUnit.run_forms' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.THalfPlaneUnit.no_wide_pair' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.THalfPlaneUnit.no_halfplane_unit_large' depends on axioms: [propext, Classical.choice, Quot.sound]
'THalfPlaneFinite.hp2_2_no_half_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'THalfPlaneFinite.hp3_2_no_half_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'THalfPlaneFinite.hp3_3_no_half_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'THalfPlaneFinite.hp4_2_no_half_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'THalfPlaneFinite.hp4_3_no_half_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'THalfPlaneFinite.hp4_4_no_half_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'THalfPlaneFinite.hp5_2_no_half_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'THalfPlaneFinite.hp5_3_no_half_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'THalfPlaneFinite.hp5_4_no_half_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'THalfPlaneFinite.hp5_5_no_half_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'THalfPlaneFinite.hp6_2_no_half_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'THalfPlaneFinite.hp6_3_no_half_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'THalfPlaneFinite.hp6_4_no_half_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'THalfPlaneFinite.hp6_5_no_half_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'THalfPlaneFinite.hp6_6_no_half_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'THalfPlaneFinite.finite_no_half_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.TPlaneShort.corner_forms' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.TPlaneShort.concave_right' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.TPlaneShort.antiparallel_first' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.TPlaneShort.antiparallel_impossible' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.TPlaneShort.no_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.TPlaneDeep.deep_left_run' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.TPlaneDeep.weak_left_run' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.TPlaneLong.antiparallel_reduced' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.TPlaneLong.concave_reduced' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.TPlaneLong.no_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.TPlaneLong.three_arms_no_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.TPlaneTwoLongBridge.no_s_neighbor' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.TPlaneTwoLongBridge.finite_bridge_impossible' depends on axioms: [propext,
'PolyominoFormal.TPlaneTwoLong.forced_Z' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.TPlaneTwoLong.no_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.t_halfplane_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.t_plane_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.normalized_T_classified' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.all_tuples_of_families' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.sorted_L_classified' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolyominoFormal.all_tuples_classified' depends on axioms: [propext, Classical.choice, Quot.sound]
