'S2xS2Quotient.backward_forward' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.forward_backward' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.tau_pow_alpha' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.tau_pow_z' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.relations_abs' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.relations_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.relations_le_ker_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.descend' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.quotient_hom_ext' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.relations_map_power' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.conjugation_zeta' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.commutator_Wa_Wb' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.commutator_Wb_zeta' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.commutator_zeta_zeta' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.zetaBlock_eq_product' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.zetaBlock_square' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.normal_form' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.group_hom_ext' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.comparison' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.comparison_Wa' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.comparison_Wb' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.comparison_zeta' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.comparison_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.unrestricted_commutator' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.unrestrictedZeta_central' depends on axioms: [propext, Quot.sound]
'S2xS2Quotient.unrestrictedZeta_zpow_eq_one_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.powerAction' depends on axioms: [propext, Quot.sound]
'S2xS2Quotient.intertwine_zpow' depends on axioms: [propext, Quot.sound]
'S2xS2Quotient.General.relations_map_power' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.General.monodromy_power_q' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.General.EvaluationSequence.modelEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.General.EvaluationSequence.modelEquiv_kernel' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.General.EvaluationSequence.modelEquiv_generator' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.General.sphereTwoModel' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.evaluation_retraction' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.evaluation_motionLoop' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.loopClass_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.evaluationPi_WaLift' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.evaluationPi_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.evaluationCoordinate_section' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.evaluationCoordinate_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.evaluation_fiberPi' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereInclusion_in_kernel' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.freeLoopEquivOfBoundaryData' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.freeLoopEquiv_generator' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.freeLoopEquiv_sphere' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.basedLoopHomeomorph' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.cubicalGroupEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoIntervalLoop' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoBasedLoop' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.fiberIdentificationZero' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.rightTranslation' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.homotopyEquivPi' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.intervalLoopTranslation' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.fiberTransport' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.fiberIdentification' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.continuous_closePath' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.loopClass_eq_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.pathChange_natural' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.homotopy_induced' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.paddingHomotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.paddingFiberPath' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.continuous_whiskeredInterval' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.evaluationContraction' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.evaluation_fiberInclusion' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.evaluation_kernel_lift' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.evaluation_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.evaluation_lifting_proved' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.evaluation_exact_proved' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.BoundaryActionData.toBoundaryData' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.freeLoopEquivOfBoundaryActionData' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.leftTranslation' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.conjugationEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.fiberConjugationEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.conjugationPrefixHomotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.motionFiberClosingPath' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.pathChange_trans' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.pathChange_loop_conjugation' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.basedLoopPiEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.basedLoopPi_comm' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.evaluation_kernel_comm' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sameEvaluation_conjugation' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.rawFiberMotionEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.rawFiberMotion_inclusion' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.transportAmbientLoop_evaluation' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.fiberMotion_action' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.windingMonodromy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.windingMonodromy_action' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.RemainingAssumptions.boundaryActionData' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.homotopyFromRealLifts' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.windingAdditionHomotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.loopClass_winding_zpow' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.mapped_winding_zpow' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.winding_betaLoop_class' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.rotationHomotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.rotationLoop_central' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.rotationLoop_winding_class' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.WaLift_sector_power_central' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.General.inclusion_power_of_conjugation' depends on axioms: [propext, Quot.sound]
'S2xS2Quotient.General.descendRelations' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereInclusion_monodromy_power' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereInclusion_sector_period' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.boundary_relations_vanish' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.quotientSphereInclusion' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.quotientSphere_equivariance' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.freeLoopModelMap' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.freeLoopModelMap_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.freeLoopModelMap_generator' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.freeLoopModelMap_sphere' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.freeLoopModelMap_injective_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.pointedInduced_homotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.pointedInduced_comp' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.fundamentalGroup_prod_ext' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.induced_diagonal' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.induced_binary_diagonal' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.intervalLoopPi_comm' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.intervalBoundary_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.intervalBoundaryZeroNullhomotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.reverseLoopHom_apply' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.intervalBoundary_difference' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.conjugationLeftTranslationHomotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.evaluationBoundary_translations' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.rotation_leftTranslation' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.evaluationBoundary_rotation_difference' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.boundarySphereClass_difference' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.boundary_coordinates_proved' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.boundary_complete_proved' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.boundary_exact_proved' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.freeLoopModelMap_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.freeLoopGroupEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.freeLoopGroupEquiv_apply' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.pathChange_homotopic' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.pathChange_independent_of_comm' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.closedInduced_homotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.closedInduced_comp' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.closedInduced_comp_of_comm' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.loopMapAssociativity' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.conjugationPathHomotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.conjugationCompositionHomotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.fiberConjugationCompositionHomotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.closedFiberConjugation_independent' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.closedFiberConjugation_homotopic' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.closedFiberConjugation_trans' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.fiberMotion_sameEvaluation' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.fiberMotion_trans' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.fiberMotion_refl' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.fiberMotionRepresentation' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.fiberMotionRepresentation_loopClass' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.fiberMotionRepresentation_sameEvaluation' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.fiberMotionRepresentation_kernel' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereMotionRepresentation' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereMotionRepresentation_Wa_power' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.rotation_transport_winding_power' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.rotation_transport_winding_apply' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.boundaryLoopMap' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.fiberPaddingHomotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.evaluationBoundary' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.boundaryFreeHomotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.induced_of_nullhomotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.evaluationBoundary_in_kernel' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.nullEvaluationSphere' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.continuous_nullWhiskeredInterval' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.kernelBoundaryHomotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.fiber_kernel_boundary_lift' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.evaluation_boundary_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.boundarySphereClass' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereInclusion_kernel_iff_boundary' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.boundary_complete_iff_coordinates' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.freeLoopModelMap_injective_iff_boundary_coordinates' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.boundaryZeroNullhomotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.evaluationBoundary_constant' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.boundarySphereClass_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.boundary_coordinates_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.freeLoopModelMap_zero_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.RemainingAssumptions.boundary_complete' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.RemainingAssumptions.ofZeroCoordinates' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.General.relations_equiv_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.SphereTwoAssumptions.groupEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.SphereTwoAssumptions.commutator_Wa_Wb' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.SphereTwoAssumptions.conjugation_zeta' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.SphereTwoAssumptions.commutator_Wb_zeta' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.SphereTwoAssumptions.commutator_zeta_zeta' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.SphereTwoAssumptions.zeta_periodic' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.SphereTwoAssumptions.zeta_product_square' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.SphereTwoAssumptions.hom_ext' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.SphereTwoAssumptions.ofPiTwoData' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.RemainingAssumptions.toTarget' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.RemainingAssumptions.groupEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.RemainingAssumptions.groupEquiv_Wa' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.RemainingAssumptions.groupEquiv_Wb' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.RemainingAssumptions.groupEquiv_zeta' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.ComponentCoverage.path_iff_sector_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.ComponentCoverage.groupEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.closePath_joined_of_class_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.moveLoopPath' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.freeLoopPathHomotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.cyclic_pi_comm' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.freeLoopSector_of_path_choice' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.freeLoopSector_of_path' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.freeLoopSector_winding' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.freeLoop_path_to_winding' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.cyclicComponentCoverage' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.freeLoop_path_iff_sector_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.cyclicFreeLoopComponents' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.cyclicFreeLoopGroupEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.continuous_euclideanSphereToSphereTwo' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.euclideanSphereToSphereTwo_surjective' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.sphereTwoPathConnectedSpace' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleQuotient_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCirclePathConnectedSpace' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.RoundCircleAssumptions.coverage' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircle_sections' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleConstants_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.freeLoopHomotopyEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircle_characterization' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.RoundCircleAssumptions.transfer' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.target_characterization' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.circleSection_project' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.circleCoverChart' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.circleReal_isCoveringMap' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.circlePathLift_project' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.circlePathLift_winding' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.windingCirclePath_class_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.circlePath_homotopic_winding' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.circleWindingHom_bijective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.circleFundamentalGroupEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.circleFundamentalGroupEquiv_generator' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.continuous_sphereMeridian' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.continuous_roundCircleHeight' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleWinding' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleMeridianLoop' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleHeight_meridian' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleWinding_generator' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleWinding_retraction' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleGenerator_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCirclePiWinding_section' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleInteger_section' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleInteger_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleIntegerSection_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleInteger_generator' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleGenerator_power_eq_one_iff' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleInteger_injective_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoordinate' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoordinate_generator' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.ConcreteRoundCircleAssumptions.toRemaining' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.ConcreteRoundCircleAssumptions.toRoundCircle' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.concrete_target_characterization' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.integerCoverChart' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.integerCover_isCoveringMap' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.integerCoverProjection_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.integerCoverDeck' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.integerCoverDeck_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.integerCoverDeck_free' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.integerCoverDeck_fiber_transitive' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.circlePathLift_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.circlePathLift_one_zero_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.simplyConnected_of_trivial_pi' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCover_isCoveringMap' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverMeridian' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCover_joined_base' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverPathConnectedSpace' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleInteger_loopClass' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleClosedLift' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleClosedLift_projection' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCover_loop_zero_winding' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverPi_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverPi_zero_winding' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverPi_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverToKernel_bijective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverKernelEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCover_simplyConnected_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.CoveredRoundCircleAssumptions.toConcrete' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.ConcreteRoundCircleAssumptions.toCovered' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.covered_assumptions_iff_concrete' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.covered_target_characterization' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleHeight_sum_sub' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleHeight_sum_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleHeight_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleHeight_eq_zero_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleHeight_eq_one_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleQuotient_eq_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereTwoCompactSpace' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCompactSpace' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeparator_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleT2Space' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverBlock' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverBlock_sections' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverBlock_deck' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverBlock_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverBlock_isClosedEmbedding' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverBlock_covers' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverBlock_range' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverBlock_adjacent_of_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverBlock_nonadjacent' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverBlock_intersection' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleChainToCover' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleChainToCover_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleChainToCover_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.locallyFinite_integer_slabs' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverBlocks_locallyFinite' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleChainToCover_isClosedMap' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleChainHomeomorph' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleChainHomeomorph_block' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleChainDeck_block' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleFiniteChainSet_blocks' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleFiniteChainSet_isCompact' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCover_compact_family_bounded' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleCover_compact_family_factors' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleCover_simplyConnected_of_finite_chains' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.finiteChain_target_characterization' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.intervalSegment' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.intervalSegment_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.interval_paths_homotopic' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.pathSegment_trans' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.pathSegment_whole' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.path_property_of_open_cover' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.pathRestrict' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.pathWithin_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.paths_homotopic_in_simplyConnected_set' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.twoSetBasePath_homotopic_right' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.simplyConnected_of_two_open_sets' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.simplyConnected_of_homotopyEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.simplyConnected_of_homeomorph' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.simplyConnected_product' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.puncturedOverlapMap_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.pathConnected_punctured_overlap' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.euclideanSpherePunctureHomeomorph' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.euclideanSpherePuncture_contractible' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.euclideanSphereTwo_simplyConnected' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.euclideanSphereToSphereTwo_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.euclideanSphereTwoHomeomorph' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereTwoSimplyConnectedSpace' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereTwoProductSimplyConnectedSpace' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleFiniteChainZeroHomeomorph' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleFiniteChainZeroSimplyConnected' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverDeck_base' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverMeridian_mem_finite' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverBlock_mem_finite' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleFiniteChain_joined_base' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleFiniteChainPathConnectedSpace' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleCover_simplyConnected_of_positive_finite_chains' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.positiveFiniteChain_target_characterization' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.coordinateSquareNorm_pos_of_dot_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereNormalize' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereNormalize_of_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereBlend_dot' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.diagonalSphereCap_isOpen' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.diagonalSphereCap_height' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereBlend_cap_dot_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.diagonalCapDeformation' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.diagonalCapDeformation_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.diagonalCapDeformation_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.diagonalCapDeformation_section' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.diagonalCapDeformation_projection' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.diagonalCapHomotopyEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.diagonalCapSimplyConnectedSpace' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleHeight_secondAntipode' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.antidiagonalSphereCap_isOpen' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.antidiagonalSphereCap_height' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.antidiagonalCapHomeomorph' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.antidiagonalCapDeformation' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.antidiagonalCapDeformation_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.antidiagonalCapDeformation_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.antidiagonalCapDeformation_section' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.antidiagonalCapDeformation_projection' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.antidiagonalCapHomotopyEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.antidiagonalCapSimplyConnectedSpace' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.quotientFamilyLift' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.quotientFamilyLift_apply' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamSet_isOpen' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamUpper_range' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamLower_range' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamUpper_isClosedEmbedding' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamLower_isClosedEmbedding' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeam_cross_eq_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamQuotient_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamQuotient_isQuotientMap' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamDeformationBefore_respects' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamDeformation' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamDeformation_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamDeformation_upper' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamDeformation_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamDeformation_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamDeformation_section' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamDeformation_projection' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamHomotopyEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamSimplyConnectedSpace' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockNeighborhoodSet' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockNeighborhoodSet_isOpen' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockNeighborhoodHeight' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockNeighborhoodProjection' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockNeighborhoodLower' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockNeighborhoodMiddle' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockNeighborhoodUpper' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockNeighborhoodLower_range' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockNeighborhoodMiddle_range' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockNeighborhoodUpper_range' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockNeighborhoodLower_isClosedEmbedding' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockNeighborhoodMiddle_isClosedEmbedding' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockNeighborhoodUpper_isClosedEmbedding' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockNeighborhood_lower_section' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockNeighborhood_upper_section' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockNeighborhood_lower_middle_eq_iff' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockNeighborhood_middle_upper_eq_iff' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockNeighborhood_lower_ne_upper' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockNeighborhoodQuotient' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockNeighborhoodQuotient_surjective' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockNeighborhoodQuotient_isQuotientMap' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockNeighborhoodSet_intersection' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockNeighborhoodSet_nonadjacent' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockNeighborhoodSet_covers' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockDeformationBefore' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockDeformationBefore_respects' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockDeformation' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockDeformation_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockDeformation_middle' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockDeformation_upper' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockDeformation_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockDeformation_one_mem_middle' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockRetraction' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockDeformation_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockRetraction_middle' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockDeformation_projection' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockHomotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockHomotopyEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockNeighborhoodSimplyConnectedSpace' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.subsetPreimageHomeomorph' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.simplyConnected_union' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleOpenChainSet' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleOpenChainSet_isOpen' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleOpenChainSet_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleOpenChainSet_succ' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleOpenChainSet_intersection' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleOpenChainSimplyConnectedSpace' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleFiniteChainSet_subset_openChain' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverSimplyConnectedSpace' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircle_zero_winding_null' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleInteger_injective_proved' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleFundamentalGroupEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleFundamentalGroupEquiv_apply' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleFundamentalGroupEquiv_generator' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleComponentCoverage' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleFreeLoopComponents' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.RoundCirclePiTwoAssumptions.toCovered' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.CoveredRoundCircleAssumptions.toPiTwo' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.piTwo_assumptions_iff_covered' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.RoundCirclePiTwoAssumptions.toRemaining' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.RoundCirclePiTwoAssumptions.groupEquiv' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.RoundCirclePiTwoAssumptions.groupEquiv_Wa' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.RoundCirclePiTwoAssumptions.groupEquiv_Wb' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.RoundCirclePiTwoAssumptions.groupEquiv_zeta' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.RoundCirclePiTwoAssumptions.groupEquiv_at' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.piTwo_target_characterization' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.genLoopPostcompose' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.genLoopPostcompose_apply' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.genLoopPostcompose_homotopic' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.genLoopPostcompose_transAt' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.homotopyGroupMap' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.homotopyGroupMap_mk' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.homotopyGroupMap_id' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.homotopyGroupMap_comp' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.cubicalSphereSquare' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.cubicalSphereSquare_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.coveringSquareLift' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.coveringSquareLift_lifts' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.coveringSquareLift_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.coveringSquareLift_edge' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.coveringSquareLift_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.coveringGenLoopLift' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.coveringGenLoopLift_projection' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.coveringGenLoop_homotopic_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.coveringPiTwoMap_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.coveringPiTwoMap_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.coveringPiTwoMulEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.coveringPiTwoEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.coveringPiTwoEquiv_mk' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverPiTwoEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverPiTwoEquiv_mk' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.liftedWindingMonodromy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverPiTwoEquiv_monodromy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.RoundCirclePiTwoAssumptions.ofCoverCoordinates' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.RoundCirclePiTwoAssumptions.coverCoordinates' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.RoundCirclePiTwoAssumptions.coverCoordinates_equivariant' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.piTwo_coordinates_on_cover_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.coverPiTwo_target_characterization' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.pathSpaceHomotopyPath' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.pathMapConcat' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.pathMapConcatHomotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.pathMapAssociativity' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.pathConcatRight' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.pathConcatLeft' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.pathConcatRightHomotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.pathConcatLeftHomotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.pathConcatRightUnit' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.pathConcatLeftUnit' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.pathRightAssociativity' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.pathLeftAssociativity' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.pathRightTranslation' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.pathLeftTranslation' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.loopBaseTransport' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.loopBaseTransport_apply' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.loopBaseTransportClosing' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.loopBaseTransportHomotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.loopBaseTransportComposition' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.loopBaseTransportUnit' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.intervalLoopBaseTransportPi' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.intervalLoopBaseTransportPi_apply' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.intervalLoopBaseTransportPi_homotopic' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.intervalLoopBaseTransportPi_trans' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.intervalLoopBaseTransportPi_refl' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoPathMulEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoPathEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoPathEquiv_homotopic' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoPathEquiv_trans' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoPathEquiv_refl' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoPathEquiv_symm_cancel' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoPathEquiv_independent' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.pathPostcompose' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.pathPostcompose_refl' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoIntervalLoop_natural' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoMap' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoMap_mk' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoMap_id' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoMap_comp' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.pointedInduced_refl' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.pointedInduced_congr' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.loopBaseTransport_natural' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.intervalLoopBaseTransportPi_natural' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoIntervalLoop_transport' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoMap_pathEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoPointedMap' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoPointedMap_independent' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoPointedMap_comp' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoPointedMap_refl' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.simplyConnectedPiTwoMap' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.simplyConnectedPiTwoMap_path' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.simplyConnectedPiTwoMap_comp' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.simplyConnectedPiTwoMap_id' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.simplyConnectedPiTwoHomeomorph' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.simplyConnectedPiTwoHomeomorph_apply' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoMonodromyOfClass' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoMonodromyOfClass_loopClass' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoMonodromy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoMonodromy_loopClass' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.loopClass_symm' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoMonodromy_winding' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoMonodromy_trivial' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoMonodromy_natural' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleDeckPiTwo' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleDeckPiTwo_path' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleDeckPiTwo_meridian' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleDeckPiTwo_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleDeckPiTwo_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleDeckPiTwoRepresentation' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleDeckPiTwo_neg' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.coveringPiTwoEquiv_apply' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverPiTwoEquiv_apply' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleDeckPiTwo_projection' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverMeridian_projection' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverMeridian_one_projection' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleDeckPiTwo_one_projection' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleDeckPiTwo_winding_projection' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleDeckPiTwo_neg_one_projection' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.liftedWindingMonodromy_eq_deck_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.RoundCirclePiTwoAssumptions.ofGeometricDeckCoordinates' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.geometricDeck_target_characterization' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.pathSpacePathHomotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.constantPathHomotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.commutationFromConjugationClosing' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.conjugationRightTranslationHomotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.fiberConjugationRightTranslationHomotopy' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.closedFiberConjugation_rightTranslation' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.pathChange_constantCast' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.closeFiberHom_eq_homeomorphPi' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.fiberIdentification_rightTranslation' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.fiberMotion_rightTranslation' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.windingMonodromy_eq_pathEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.windingMonodromy_independent' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.liftedWindingMonodromy_eq_deck' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.RoundCircleDeckAssumptions.toPiTwo' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.RoundCirclePiTwoAssumptions.toDeck' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.deck_assumptions_iff_piTwo' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.RoundCircleDeckAssumptions.groupEquiv' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.RoundCircleDeckAssumptions.groupEquiv_Wa' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.RoundCircleDeckAssumptions.WbLoop' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.RoundCircleDeckAssumptions.zetaLoop' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.RoundCircleDeckAssumptions.groupEquiv_Wb' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.RoundCircleDeckAssumptions.groupEquiv_zeta' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.RoundCircleDeckAssumptions.groupEquiv_at' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.deck_target_characterization' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.standardFreeLoopGroupEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.A' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.B' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.relation' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.relations' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.quotient' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.tau_zpow_z' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.diagonalCoordinate' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.secondCoordinate' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.diagonalCoordinate_succ' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.coordinates' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.coordinates_A' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.coordinates_B' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.coordinates_relation' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.relations_le_coordinates_ker' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.quotientCoordinates' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.quotientCoordinates_quotient' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.quotient_relation' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.fromCoordinates' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.fromCoordinates_alpha' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.fromCoordinates_z' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.fromCoordinates_second' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.fromCoordinates_diagonal' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.quotientCoordinates_fromCoordinates' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.fromCoordinates_coordinates' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.basisEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.coordinates_ker' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.evaluate' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.evaluate_A' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.evaluate_B' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.relations_le_evaluate_ker' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.quotientEvaluate' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.quotientEvaluate_quotient' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.basisMap' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.basisMap_alpha' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.basisMap_z' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.quotientEvaluate_bijective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.basisMap_bijective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.basisEquivOfExact' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.basisMap_equivariant' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.genLoopPair' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.genLoopPair_homotopic' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoProductMap' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoProductMap_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoProductMap_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoProductEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoProductEquiv_fst' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoProductEquiv_snd' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoMap_const' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.simplyConnectedPiTwoMap_strict' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.simplyConnectedPiTwoMap_const' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.simplyConnectedPiTwoMap_pair' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.simplyConnectedPiTwoMap_factors' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.simplyConnectedPiTwoMap_prodMk_comp' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.simplyConnectedPiTwoProductMap' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.simplyConnectedPiTwoProductMap_comp' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.linearMap_pair' depends on axioms: [propext, Quot.sound]
'S2xS2Quotient.Topology.linearMap_pair_components' depends on axioms: [propext, Quot.sound]
'S2xS2Quotient.Topology.linearMap_first_transport' depends on axioms: [propext, Quot.sound]
'S2xS2Quotient.Topology.linearMap_second_transport' depends on axioms: [propext, Quot.sound]
'S2xS2Quotient.Topology.simplyConnectedPiTwoProductMap_diagonal' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.simplyConnectedPiTwoProductMap_graph' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereAntipodeMap' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereAntipodePiTwo' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereDiagonalMap' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereAntidiagonalMap' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockPiTwo' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockFirst' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockSecond' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockPiTwo_pair' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockPiTwo_diagonal' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockPiTwo_antidiagonal' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockPiTwo_sections' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockPiTwo_deck' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockFirst_deck' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockSecond_deck' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockEvaluation' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlock_section_relation' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlock_relations_in_kernel' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockCoordinates' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockCoordinates_alpha' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockCoordinates_z' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockCoordinates_equivariant' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.RoundCircleBlockAssumptions.toDeck' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.block_model_characterization' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.block_target_characterization' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.pathFinalSegment' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.continuous_pathFinalSegment' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.homotopyImageLoop' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.homotopyWhiskeredLoop' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.continuous_homotopyWhiskeredLoop' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.homotopyLoopMapPadded' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.homotopyLoopMap' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.intervalLoopMap_homotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoMap_homotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.simplyConnectedPiTwoMap_homotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.genLoopPostcomposeAt' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.simplyConnectedPiTwoMap_class' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereSquareHeight' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereSquareDenominator' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereSquareDenominator_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereSquareMap' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereSquareMap_boundary' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereCube' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereCubeClass' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereFirstReflection' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereFirstReflection_north' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereSquareMap_reflection' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereCube_reflection' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereCubeClass_reflection' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereReflectionRotationPoint' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.continuous_sphereReflectionRotationPoint' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.sphereReflectionRotationPoint_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereReflectionRotationPoint_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereReflectionAntipodeHomotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereCubeClass_antipode' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleExplicitCoordinates' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleExplicitCoordinates_equivariant' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.RoundCircleExplicitBlockAssumptions.toBlocks' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.RoundCircleExplicitBlockAssumptions.toDeck' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.RoundCircleExplicitBlockAssumptions.groupEquiv' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.explicit_block_model_characterization' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.explicit_block_target_characterization' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.BasedCompactExhaustion.base' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.BasedCompactExhaustion.inclusion' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.BasedCompactExhaustion.transition' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.BasedCompactExhaustion.mapToSpace' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.BasedCompactExhaustion.transitionMap' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.BasedCompactExhaustion.transitionMap_refl' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.BasedCompactExhaustion.transitionMap_trans' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.BasedCompactExhaustion.mapToSpace_transition' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.BasedCompactExhaustion.representative_factors' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.BasedCompactExhaustion.mapToSpace_jointly_surjective' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.BasedCompactExhaustion.homotopy_detected' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.BasedCompactExhaustion.mapToSpace_eq_iff' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.BasedCompactExhaustion.mapToSpace_zero_iff' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleSymmetricOpenChain_monotone' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleCompactExhaustion' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCirclePiTwoStageSimplyConnected' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCirclePiTwo_finite_representation' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCirclePiTwo_finite_equality' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCirclePiTwo_finite_nullhomotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.simplyConnectedPiTwoHomotopyEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.simplyConnectedPiTwoHomotopyEquiv_apply' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.simplyConnectedPiTwoHomotopyEquiv_symm_apply' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Blocks.indexBound' does not depend on any axioms
'S2xS2Quotient.Blocks.indexBound_mono' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.finiteIndexTransition' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.finiteInclusion' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.finiteTransition' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.finiteInclusion_single' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.finiteTransition_single' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.finiteInclusion_transition' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.finiteInclusion_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.raw_support_bounded' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Blocks.finiteInclusion_jointly_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleStageBlock_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleStageBlock' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleStageBlockPiTwo' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleStageBlockPiTwo_projection' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleStageBlockPiTwo_transition' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockSphereVector' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleStageSphere' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockSphere' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockEvaluation_as_linearCombination' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleStageSphere_projection' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleStageSphere_transition' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleFiniteBlockEvaluation' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleFiniteBlockEvaluation_projection' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleFiniteBlockEvaluation_transition' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.RoundCircleFiniteBlockAssumptions.cover_spanning' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.RoundCircleFiniteBlockAssumptions.cover_relations' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.RoundCircleFiniteBlockAssumptions.toExplicit' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.RoundCircleFiniteBlockAssumptions.groupEquiv' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.finite_block_model_characterization' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.finite_block_target_characterization' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockNeighborhoodPiTwo' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamPiTwo' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockNeighborhoodPiTwo_apply' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamPiTwo_symm_apply' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamSet_subset_rightBlock' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamSet_subset_leftBlock' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamToRightBlock' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamToLeftBlock' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamToRightBlock_section' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamToLeftBlock_section' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamToRightBlock_retraction' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamToLeftBlock_retraction' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamPiTwo_right' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamPiTwo_left' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamPiTwo_left_sphereClass' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.simplyConnected_isOneConnected' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.simplyConnectedHurewicz' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.simplyConnectedHurewicz_apply' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.simplyConnectedPiTwoMap_eq_imported_map' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.simplyConnectedHurewicz_naturality' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.spherePiTwoIntEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.spherePiTwo_exists_generator' depends on axioms: [propext, Classical.choice, Quot.sound]
'Submission.IsNConnected.absoluteHurewiczAddEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'Submission.absoluteHurewiczAdd_naturality' depends on axioms: [propext, Classical.choice, Quot.sound]
'Submission.hgrpSphereSelfIsoZ' depends on axioms: [propext, Classical.choice, Quot.sound]
'Submission.pi2_sphere_two_at_mulEquiv_int' depends on axioms: [propext, Classical.choice, Quot.sound]
'Submission.mayerVietoris_exact_δ_iota' depends on axioms: [propext, Classical.choice, Quot.sound]
'Submission.mayerVietoris_exact_iota_kappa' depends on axioms: [propext, Classical.choice, Quot.sound]
'Submission.mayerVietoris_exact_kappa_δ' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.simplyConnected_homologyOne_subsingleton' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.homologySumEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.homologySumEquiv_symm_fst' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.homologySumEquiv_symm_snd' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.homologySumEquiv_fst' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.homologySumEquiv_snd' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.homologySumEquiv_iota' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.homologyKappa_pair' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.homology_union_difference_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.homology_union_difference_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.simplyConnectedPiTwoBasepoint' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.simplyConnectedPiTwoBasepoint_apply' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.simplyConnectedPiTwoMap_changeTarget' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.simplyConnectedPiTwoMap_changeSource' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.simplyConnectedPiTwoBasepoint_naturality' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.subspaceInclusion' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.intersectionInclusionLeft' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.intersectionInclusionRight' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwo_union_difference_hurewicz' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwo_union_difference_exact_at' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwo_union_difference_surjective_at' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwo_union_sum_exact_at' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwo_union_sum_surjective_at' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwo_union_sum_basepoint' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoUnionSum' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoUnionRelation' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoUnionSum_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoUnionSum_ker' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoUnionQuotientEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoUnionQuotientEquiv_mk' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwo_union_sum_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwo_union_sum_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.DiagonalGluing.extensionMap' depends on axioms: [propext, Quot.sound]
'S2xS2Quotient.DiagonalGluing.extensionMap_apply' depends on axioms: [propext, Quot.sound]
'S2xS2Quotient.DiagonalGluing.gluing_relation' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.DiagonalGluing.normalForm' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.DiagonalGluing.extensionMap_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.DiagonalGluing.extensionMap_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.DiagonalGluing.extensionEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.DiagonalGluing.extensionEquiv_apply' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.DiagonalGluing.extensionEquiv_old' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.DiagonalGluing.extensionEquiv_new' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoSubspaceUnionMap' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoSubspaceUnion_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoSubspaceUnion_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.piTwoSubspaceUnion_ker' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleOpenChainSet_subset_succ' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleNextBlockSet_subset_succ' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamSet_subset_chain' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleChainIntoNext' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleNextBlockIntoChain' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamIntoChain' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleChainIntersectionHomeomorph' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleOpenChainPiTwoGluing' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleOpenChainPiTwoRelation' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleOpenChainPiTwoGluing_exact' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleOpenChainPiTwoGluing_diagonal' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleOpenChainPiTwoStepEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleOpenChainPiTwoStepEquiv_apply' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleOpenChainPiTwoStepEquiv_old' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleChainIntoNext_piTwo_injective' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleOpenChainSphereCoordinates' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleOpenChainPiTwoIntCoordinates' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCirclePiTwoStageIntCoordinates' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.LinearGluing.kernel_compatible' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.LinearGluing.descend' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.LinearGluing.descend_pair' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.LinearGluing.descend_left' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.LinearGluing.descend_right' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockNeighborhoodSet_subset_chain' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockNeighborhoodIntoChain' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleOpenChainBlock' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleChainBlockPiTwo' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleBlockNeighborhoodPiTwo_symm_apply' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleChainBlockPiTwo_neighborhood' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleChainBlockPiTwo_intoNext' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleChainBlockPiTwo_last' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleChainBlockPiTwo_zero_surjective' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleChainIndex' does not depend on any axioms
'S2xS2Quotient.Topology.RoundCircleChainRaw' depends on axioms: [propext, Quot.sound]
'S2xS2Quotient.Topology.roundCircleChainIndexNext' depends on axioms: [propext, Quot.sound]
'S2xS2Quotient.Topology.roundCircleChainSphere' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleChainEvaluation' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleChainSphere_intoNext' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleChainEvaluation_intoNext' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleChainEvaluation_single' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleChainEvaluation_block' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleChainEvaluation_surjective' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleChainIndexToFinite' depends on axioms: [propext, Quot.sound]
'S2xS2Quotient.Topology.roundCircleChainSphere_toFinite' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleChainEvaluation_toFinite' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleFiniteBlockEvaluation_surjective_of_sphereGeneration' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.SphereClassPrimitive' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereClassEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereClassEquiv_apply' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereClassIntCoordinates' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereClassIntCoordinates_class' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereAntipodePiTwo_eq_neg_of_generation' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.sphereBlockCoordinates' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereBlockCoordinates_apply' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereBlockCoordinates_first' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereBlockCoordinates_second' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereBlockCoordinates_sections' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleChainBlockPiTwo_zero_injective' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleChainBlockPiTwoZeroEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleChainBlockPiTwoZeroEquiv_apply' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamIntoChain_section' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleSeamIntoChain_piTwo' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleChainCoefficientMap_exists' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleFiniteBlockEvaluation_single' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleFiniteCoefficientMap_exists' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleFiniteBlock_relations_of_spherePrimitive' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.SphereClassPrimitive.finiteBlocks' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.SphereClassPrimitive.coverBasis' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.SphereClassPrimitive.coverBasis_apply' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.SphereClassPrimitive.coverBasis_equivariant' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.SphereClassPrimitive.groupEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphere_primitive_model_characterization' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.sphere_primitive_target_characterization' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.sphereSquareHeight_antitone' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereSquareScale_unique' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereSquareScale_exists' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.primitive_of_endomorphism_images' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereClassPrimitive_of_cubical_quotient' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.sphereSquareMap_eq_north_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereSquareMap_north_coordinate_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereSquareMap_stereographic' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereSquareMap_injective_off_boundary' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.cube_centered_coordinate_abs' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereCube_height_zero_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereCube_fibres' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereTwo_eq_north_of_last' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereSquareMap_of_stereographic' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereCube_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereCube_isQuotientMap' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.sphereCubeClass_primitive' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleFiniteBlockAssumptions_proved' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverDeckData' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverBasis' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverBasis_apply' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverBasis_alpha' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverBasis_z' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverBasis_equivariant' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverBasis_deck_alpha' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleCoverBasis_deck_z' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleModelGroupEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleModelGroupEquiv_Wa' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleModelGroupEquiv_Wb' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircleModelGroupEquiv_zeta' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircle_model_characterization' depends on axioms: [propext, Classical.choice, Quot.sound]
'S2xS2Quotient.Topology.roundCircle_target_characterization' depends on axioms: [propext, Classical.choice, Quot.sound]
