'FRC.Algebra.quarter_turn_exists' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.two_ne_zero_shell' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.klein_orbit_four' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.card_fourth_roots' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.quarter_turn' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.affine_frame' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.meridian_involution' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.framed_integer_window' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.scale_periodic' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.complex_chart_zero_divisor' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.no_south_pole' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.s13_quarter_turn' depends on axioms: [propext, Quot.sound]
'FRC.Algebra.euclidSteps' does not depend on any axioms
'FRC.Algebra.euclid_step_count' does not depend on any axioms
'FRC.Algebra.approx_obstruction' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.root_iff_not_coprime' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.tower_density' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.circle_net' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.group_law_defect' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.AxisAlg' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.scalars' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.card_axisAlg' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.card_scalars' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.axis_field' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.psiK' depends on axioms: [propext, Quot.sound]
'FRC.Algebra.psiK_apply' depends on axioms: [propext, Quot.sound]
'FRC.Algebra.axis_split_equiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.axis_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.axis_group' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.winPairs' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.halfPairs' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.card_halfPairs' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.card_image_le_of_neg' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.quat_pow_height' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.readback_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.p01004' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.p01005' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.p01006' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.p01011' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.p01013' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.p01015' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.p01027' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.p01019' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.p01026' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.p01028' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.p01032' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.p01033' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Algebra.p01020' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Causality.no_causal_root' depends on axioms: [propext, Quot.sound]
'FRC.Causality.neg_sq_is_square' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Causality.absorb' depends on axioms: [propext, Quot.sound]
'FRC.Causality.aniso_tx' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Causality.boost_preserves' depends on axioms: [propext, Quot.sound]
'FRC.Causality.boost_comp' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Causality.boost_orthogonal' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Causality.gamma_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Causality.gamma_velocity' depends on axioms: [propext, Quot.sound]
'FRC.Causality.velocity_addition' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Causality.p03006' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Causality.p03007' depends on axioms: [propext, Quot.sound]
'FRC.Causality.p03009' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Causality.p03013' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Causality.p03014' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.Dom' does not depend on any axioms
'FRC.Dimensions.L' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.T' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.flag' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.QA' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.U' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.U_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.U_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.U_add_neg' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.U_neg_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.U_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.Uunit' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.Uhom' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.Uhom_apply' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.Uhom_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.fibre_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.graded' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.fibre_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.coeff_sum_single' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.monomial' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.monomial_units' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.single_mem_grade_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.kappa_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.two_kappa_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.three_kappa_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.four_kappa' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.three_kappa' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.nat_mul_eq_zero_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.two_mul_eq_zero_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.four_mul_eq_zero_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.unit_odd' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.unit_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.flag_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.four_smul_flag' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.two_smul_flag' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.two_smul_flag_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.three_smul_flag_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.addOrderOf_flag' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.addOrderOf_neg_flag' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.meridian_transport' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.record' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.record_natCast' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.record_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.record_range' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.two_smul_of_mem_parity' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.record_mem_parity_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.deltaS' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.deltaS_involutive' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.deltaS_generators' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.four_domains' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.energy' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.mom' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.deltaC' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.deltaC_involutive' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.deltaC_generators' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.flagged_readings' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.flag_inaccessible' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.no_flag_of_space' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.two_mul_eq_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.order_four_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.order_two_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.unique_order_four_subgroup' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.operator_four_cycle' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.crossing_order_four' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.invariant_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.half_period_invariant_not_neutral' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.flag_moves' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.quarter_turn_law' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.sigma_twist' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.dilation_character' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.witnesses13' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.action_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.quartet_param' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.pairing_closure' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.cancellation' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.normalisation' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.index_two' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.scale_from_constants' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.exponent_faces' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.G_unique' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.linkage' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.pair_consequences' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.sign_assignments' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.isSquare_neg_two' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.h_form' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.omega_two_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.residues_exist' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.admissibility_residues' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.carrier233' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.carrierLab' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.Lab' does not depend on any axioms
'FRC.Dimensions.realize' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.realize_add' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.realize_flag' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.speedL' does not depend on any axioms
'FRC.Dimensions.timeL' does not depend on any axioms
'FRC.Dimensions.spaceL' does not depend on any axioms
'FRC.Dimensions.flagL' does not depend on any axioms
'FRC.Dimensions.energyL' does not depend on any axioms
'FRC.Dimensions.massL' does not depend on any axioms
'FRC.Dimensions.accelL' does not depend on any axioms
'FRC.Dimensions.forceL' does not depend on any axioms
'FRC.Dimensions.momL' does not depend on any axioms
'FRC.Dimensions.actionL' does not depend on any axioms
'FRC.Dimensions.powerL' does not depend on any axioms
'FRC.Dimensions.pressureL' does not depend on any axioms
'FRC.Dimensions.gravL' does not depend on any axioms
'FRC.Dimensions.kBL' does not depend on any axioms
'FRC.Dimensions.thetaL' does not depend on any axioms
'FRC.Dimensions.mechanical_domains' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.geometric_conversions' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.temperature_domain' does not depend on any axioms
'FRC.Dimensions.quartet_flags' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.equal_crossing_flag_free' depends on axioms: [propext]
'FRC.Dimensions.comparison_examples' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.local_recovery' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.embed' does not depend on any axioms
'FRC.Dimensions.embed_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.realize_faithful' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.window_ladder' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.examples13' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.recovery13' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.energy_momentum' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.window_neutrality' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.pendulum_kernel' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.root_pair' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.p10012' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.p10013' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.p10015' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.p10016' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.p10017' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.p10018' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.p10019' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.p10022' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.p10025' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.p10026' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.p10027' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.p10028' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.p10034' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.p10035' does not depend on any axioms
'FRC.Dimensions.p10036' depends on axioms: [propext, Quot.sound]
'FRC.Dimensions.p10037' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.p10038' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.p10039' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.p10046' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.p10048' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.p10049' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dimensions.p10050' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.Ext.cayley' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.Ext.norm_ofBase_mul' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.Ext.norm_one_add_kw' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.Ext.norm_one_sub_kw' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.Ext.norm_conj' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.Ext.norm_inv' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.Ext.one_sub_nu_sq_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.Ext.cayley_norm' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.Ext.conjHom' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.Ext.conjHom_apply' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.Ext.ofBaseHom' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.Ext.ofBaseHom_apply' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.Ext.norm_one' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.Ext.normOneGroup' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.Ext.mem_normOneGroup' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.Ext.conjUnits' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.Ext.conjUnits_val' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.Ext.boost' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.Ext.boost_def' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.Ext.boost_val' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.Ext.boost_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.Ext.boost_eq_one_iff' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.Ext.exists_boost_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.Ext.equivProd' does not depend on any axioms
'FRC.Dirac.Ext.card_ext' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.Ext.baseUnits' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.Ext.card_normOneGroup' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.inv_square_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.neg_two_square_iff' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.three_kappa_pow' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.sq_eq_one_cases' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.neg_inv_of_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.three_quarters' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.half_neg' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.four_ne_zero_of_two' depends on axioms: [propext]
'FRC.Dirac.named_residues' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.cayley_unitary' depends on axioms: [propext, Classical.choice]
'FRC.Dirac.cayley_periodic' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.translation_nilpotent' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.kinetic_nilpotent' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.cayley_period' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.herm' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.herm_star' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.herm_add_right' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.herm_sub_right' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.herm_smul_right' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.herm_add_left' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.herm_sub_left' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.herm_smul_left' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.herm_nondegenerate' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.translate' does not depend on any axioms
'FRC.Dirac.herm_translate' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.herm_translate_adjoint' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.laplacian' depends on axioms: [propext]
'FRC.Dirac.hamiltonian' depends on axioms: [propext]
'FRC.Dirac.herm_laplacian' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.herm_hamiltonian' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.drive' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.chi' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.drive_chi' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.drive_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.chi_isotropy' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.exceptional_eigen' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.sector_separation' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.dispersion_generic' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.dispersion' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.loss_factor_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.unit_loss_factor_one' depends on axioms: [Quot.sound]
'FRC.Dirac.power_map_count' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.Ext.boost_range' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.Ext.normOne_cyclic' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.Ext.torus_period' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.Ext.order_three_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.Ext.cayley_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.Ext.cayley_gauge' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.class_datum' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.form_class' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.ext_square' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.nu_factorisation' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.norm_growth' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.two_g_class' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.latitude_identities' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.σ1' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.σ2' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.σ3' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.J' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.β' depends on axioms: [Quot.sound]
'FRC.Dirac.ρ' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.γ0' depends on axioms: [Quot.sound]
'FRC.Dirac.γ1' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.γ2' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.γ3' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.pauli' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.β_sq' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.ρ_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.β_ρ_anticomm' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.clifford' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.Mγ' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.Xγ' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.powers' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.Mγ_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.Xγ_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.spin_conjugation' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.spinor_twist' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.σ1_dagger' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.σ3_dagger' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.J_dagger' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.σ2_dagger' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.gamma_dagger' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.twist_adjoint' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.Mγ_dagger' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.lift_adjoint' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.lift_transport' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.Aent' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.Bent' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.boost_entries' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.spin_conjugation_AB' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.shell13' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.shell17' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.carrier_constants' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.parity_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.drive_nonsquare' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.Ext' does not depend on any axioms
'FRC.Dirac.Ext.zero_re' does not depend on any axioms
'FRC.Dirac.Ext.zero_im' does not depend on any axioms
'FRC.Dirac.Ext.one_re' does not depend on any axioms
'FRC.Dirac.Ext.one_im' does not depend on any axioms
'FRC.Dirac.Ext.add_re' does not depend on any axioms
'FRC.Dirac.Ext.add_im' does not depend on any axioms
'FRC.Dirac.Ext.neg_re' depends on axioms: [propext]
'FRC.Dirac.Ext.neg_im' depends on axioms: [propext]
'FRC.Dirac.Ext.sub_re' does not depend on any axioms
'FRC.Dirac.Ext.sub_im' does not depend on any axioms
'FRC.Dirac.Ext.mul_re' does not depend on any axioms
'FRC.Dirac.Ext.mul_im' does not depend on any axioms
'FRC.Dirac.Ext.nsmul_re' does not depend on any axioms
'FRC.Dirac.Ext.nsmul_im' does not depend on any axioms
'FRC.Dirac.Ext.zsmul_re' does not depend on any axioms
'FRC.Dirac.Ext.zsmul_im' does not depend on any axioms
'FRC.Dirac.Ext.ofBase' does not depend on any axioms
'FRC.Dirac.Ext.w' does not depend on any axioms
'FRC.Dirac.Ext.conj' depends on axioms: [propext]
'FRC.Dirac.Ext.norm' does not depend on any axioms
'FRC.Dirac.Ext.ofBase_re' does not depend on any axioms
'FRC.Dirac.Ext.ofBase_im' does not depend on any axioms
'FRC.Dirac.Ext.w_re' does not depend on any axioms
'FRC.Dirac.Ext.w_im' does not depend on any axioms
'FRC.Dirac.Ext.conj_re' depends on axioms: [propext]
'FRC.Dirac.Ext.conj_im' depends on axioms: [propext]
'FRC.Dirac.Ext.w_sq' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.Ext.conj_mul' depends on axioms: [propext]
'FRC.Dirac.Ext.conj_add' depends on axioms: [propext]
'FRC.Dirac.Ext.conj_conj' depends on axioms: [propext]
'FRC.Dirac.Ext.conj_one' depends on axioms: [propext]
'FRC.Dirac.Ext.mul_conj' depends on axioms: [propext]
'FRC.Dirac.Ext.norm_mul' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.Ext.ofBase_mul' depends on axioms: [propext]
'FRC.Dirac.Ext.ofBase_add' depends on axioms: [propext]
'FRC.Dirac.Ext.ofBase_one' does not depend on any axioms
'FRC.Dirac.Ext.ofBase_zero' does not depend on any axioms
'FRC.Dirac.Ext.ofBase_injective' does not depend on any axioms
'FRC.Dirac.Ext.conj_ofBase' depends on axioms: [propext]
'FRC.Dirac.Ext.conj_w' depends on axioms: [propext]
'FRC.Dirac.Ext.conj_eq_self_iff' depends on axioms: [propext]
'FRC.Dirac.Ext.conj_eq_neg_iff' depends on axioms: [propext]
'FRC.Dirac.Ext.star_def' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.Ext.eq_re_add_im_w' depends on axioms: [propext]
'FRC.Dirac.Ext.instZero' does not depend on any axioms
'FRC.Dirac.Ext.instOne' does not depend on any axioms
'FRC.Dirac.Ext.instAdd' does not depend on any axioms
'FRC.Dirac.Ext.instNeg' depends on axioms: [propext]
'FRC.Dirac.Ext.instSub' does not depend on any axioms
'FRC.Dirac.Ext.instMul' does not depend on any axioms
'FRC.Dirac.Ext.instSMulNat' does not depend on any axioms
'FRC.Dirac.Ext.instSMulInt' does not depend on any axioms
'FRC.Dirac.Ext.instCommRing' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.Ext.instStarRing' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.Ext.norm_eq_zero_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.Ext.instInv' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.Ext.inv_def' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.Ext.mul_inv_cancel'' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.Ext.field' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.p08002' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.p08005' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.p08008' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.p08009' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.p08010' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.p08011' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.p08012' depends on axioms: [propext, Quot.sound]
'FRC.Dirac.p08013' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.p08016' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.p08018' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.p08019' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.p08020' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.p08022' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.p08025' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.p08026' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.p08027' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.p08029' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.p08030' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.p08031' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.p08032' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.p08035' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.p08036' depends on axioms: [Quot.sound]
'FRC.Dirac.p08037' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.p08039' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.p08040' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Dirac.p08041' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.cardinality' depends on axioms: [propext, Quot.sound]
'FRC.Entropy.quarter_turn_of_sq' depends on axioms: [propext, Quot.sound]
'FRC.Entropy.quarter_turn' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.area_law_chart' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.triality_centre' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.c_square' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.carrierLab' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.horizon_quarter_closure' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.dictionary' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.milgrom_rebooking' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.octant_sector_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.closure_budget' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.octant_character' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.octant_exists_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.octant_second_face' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.lcdmAge' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.octant_inversion' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.channel_one_consistency' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.cluster_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.fluid_w' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.channel_one_numeral' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.lcdmScale' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.lcdmScale_cube' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.lcdmScale_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.lcdm_hasDerivAt' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.lcdm_friedmann' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.lcdmScale_eq_one_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.lcdm_age' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.lcdm_rate_today' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.exp_tail_bounds'' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.age_bracket' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.count_face' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.capacity_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.hydrogen_units' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.nesting_lab' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.additive_window' depends on axioms: [propext, Quot.sound]
'FRC.Entropy.lock_recurrence' depends on axioms: [propext, Quot.sound]
'FRC.Entropy.shells_of_capacity' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.fusion_capacity' depends on axioms: [propext, Quot.sound]
'FRC.Entropy.two_faces' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.lambda_face' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.wall_exit' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.hubble_on_bh_line' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.running_floor' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.record_depth' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.octant_chart' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.tanh_octant_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.age_rate_locus' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.tanh_eq_exp_two_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.exp_tail_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.exp_three_pi_four_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.tanh_octant_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.locus_bracket' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.landing_bracket' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.p14001' depends on axioms: [propext, Quot.sound]
'FRC.Entropy.p14002' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.p14010' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.p14016' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.p14017' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.p14044' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.p14046' depends on axioms: [propext, Quot.sound]
'FRC.Entropy.p14047' depends on axioms: [propext, Quot.sound]
'FRC.Entropy.p14048' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.p14018' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.p14019' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.p14020' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.p14022' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.p14023' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.p14024' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.p14025' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.p14026' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.p14027' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.p14028' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.p14029' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.p14030' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.p14031' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.p14032' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.p14033' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.p14034' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.p14035' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.p14036' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.p14037' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.p14038' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Entropy.p14039' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.wallisV' depends on axioms: [propext, Quot.sound]
'FRC.Epi.wallisW' depends on axioms: [propext, Quot.sound]
'FRC.Epi.fixSet' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.card_fixing' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.pow_card_fixSet' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.rencontres' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.rencontres_rat' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.rencontres_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.rencontres_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.expNegOneSum' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.expNegOneSum_succ' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.hasSum_expNegOneSum' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.tendsto_expNegOneSum' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.antitone_inv_factorial' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.expNegOneSum_even_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.le_expNegOneSum_odd' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.numDerangements_eq_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.tailDelta' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.tailDelta_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.tailDelta_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.tailDelta_succ' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.tailDelta_strict' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.epsChain' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.exp_neg_one_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.numDerangements_eq_tailDelta' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.tailDelta_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.numDerangements_pos_real' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.epsChain_sub_exp' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.epsChain_sign' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.epsChain_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.epsChain_enclosure' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.numDerangements_2' does not depend on any axioms
'FRC.Epi.numDerangements_3' does not depend on any axioms
'FRC.Epi.numDerangements_4' does not depend on any axioms
'FRC.Epi.numDerangements_5' does not depend on any axioms
'FRC.Epi.numDerangements_6' does not depend on any axioms
'FRC.Epi.numDerangements_7' does not depend on any axioms
'FRC.Epi.numDerangements_8' does not depend on any axioms
'FRC.Epi.numDerangements_9' does not depend on any axioms
'FRC.Epi.numDerangements_10' does not depend on any axioms
'FRC.Epi.numDerangements_11' does not depend on any axioms
'FRC.Epi.numDerangements_12' does not depend on any axioms
'FRC.Epi.numDerangements_13' does not depend on any axioms
'FRC.Epi.numDerangements_14' does not depend on any axioms
'FRC.Epi.numDerangements_15' does not depend on any axioms
'FRC.Epi.numDerangements_16' does not depend on any axioms
'FRC.Epi.numDerangements_17' does not depend on any axioms
'FRC.Epi.numDerangements_18' does not depend on any axioms
'FRC.Epi.binary64E' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.readout_binary64' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.roundTo' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.cellDist' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.floor_eq_of_abs_sub_lt' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.roundTo_eq_of_lt_cellDist' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.floor_sub_abs_le_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.roundTo_sub_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.readout_within_ulp' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.readout_plateau' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.readout_six_bits' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.derangement_cost' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.log_one_add_inv_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.compound_cost' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.joint_return_tally' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.centralBinom_mul_factorial_sq' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.wallis_chain_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.tendsto_wallis_chain' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.arctanSum' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.arctanTerm_antitone' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.arctanTerm_hasSum' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.arctanSum_error' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.arctan_pairing' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.machin' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.machin_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.machin_hundred_digits' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.machinLo' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.machinHi' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.machin_pairing' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.pi_bracket_24' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.binary64Pi' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.readout_binary64_pi' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.leibnizSum' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.gregory_brackets' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.rounding_chain' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.kurepa' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.altFact' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.neg_one_pow_mul_self' depends on axioms: [propext, Quot.sound]
'FRC.Epi.neg_one_pow_sub_of_pow_eq_one' depends on axioms: [propext, Quot.sound]
'FRC.Epi.natCast_pred_sub' depends on axioms: [propext, Quot.sound]
'FRC.Epi.factorial_mul_reflect' depends on axioms: [propext, Quot.sound]
'FRC.Epi.wilson_reflection' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.ascFactorial_reflect' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.derangements_wall' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.derangements_succ_cast' depends on axioms: [propext, Quot.sound]
'FRC.Epi.neg_one_pow_pred_of_odd' depends on axioms: [propext, Quot.sound]
'FRC.Epi.derangements_antiperiodic' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.series_duals' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.tower_e_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.tail_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.factorial_ne_zero_zmod' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.factorial_mul_prime_eq_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.wilson_reflection_zmod' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.derangements_wall_zmod' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.terminal_residue' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.derangements_antiperiodic_zmod' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.series_duals_zmod' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.tower_e_exact_zmod' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.tail_identity_zmod' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.blind_iff_collision' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.sq_eq_one_of_eq_neg_one_pow' depends on axioms: [propext, Quot.sound]
'FRC.Epi.choose_pred_eq_neg_one_pow' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.half_wall_generic' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.quarter_wall_generic' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.first_revival_generic' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.tower_pi_generic' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.natCast_ne_zero_of_lt' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.two_ne_zero_zmod' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.legibility_window' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.half_wall_terminus' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.quarter_wall_invariant' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.choose_two_mul_pow_succ' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.choose_two_mul_pow' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.first_revival' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.tower_pi_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.cayley' depends on axioms: [propext, Quot.sound]
'FRC.Epi.cayley_values' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.cayley_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.calibration_ne_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.exp_I_ne_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.index_condition' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.index_condition_pow' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.index_condition_shell' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.calibrated_778933' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.centralBinom_succ_rat' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.centralBinom_pos_rat' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.wallis_width' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.wallisV_succ' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.wallisV_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.wallisV_strictMono' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.wallisW_succ' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.wallisW_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.wallisW_strictAnti' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.centralBinom_real' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.wallisV_real' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.wallisW_real' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.wallis_enclosure' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.fq' depends on axioms: [propext]
'FRC.Epi.fq_spec' depends on axioms: [propext, Quot.sound]
'FRC.Epi.fq_four_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.second_order_generic' depends on axioms: [propext, Quot.sound]
'FRC.Epi.one_add_mul_pow' depends on axioms: [propext]
'FRC.Epi.oeis_generic' depends on axioms: [propext, Quot.sound]
'FRC.Epi.sum_range_two_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.harmonic_generic' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.eisenstein_generic' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.two_pow_pred_dvd' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p_sq_eq_zero' depends on axioms: [propext, Quot.sound]
'FRC.Epi.p_mul_natCast_eq_zero_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p_mul_intCast_eq_zero_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.four_pow_pred' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.piWieferich_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.half_wall_second_order' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.choose_pred_zmod' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p_mul_congr' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.choose_succ_mul_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.coprime_succ_sq' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.choose_succ_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.two_pow_sub_two' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p_mul_eq_zero_iff_cast' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.cast_inv_succ' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.harmonic_pred_eq_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p_mul_eq_iff_cast' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.eisenstein' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.piWieferich_iff_harmonic' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.piWieferich_iff_oeis' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p13013' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p13014' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p13016' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p13018' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p13019' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p13020' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p13021' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p13023' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p13024' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p13025' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p13026' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p13027' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p13028' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p13029' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p13030' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p13033' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p13066' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p13034' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p13035' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p13036' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p13037' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p13038' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p13042' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p13067' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p13045' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p13069' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p13047' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p13048' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p13049' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p13050' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Epi.p13057' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.sum_pow_eq_zero_of_ne_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.W' depends on axioms: [propext, Quot.sound]
'FRC.Fourier.J' depends on axioms: [propext, Quot.sound]
'FRC.Fourier.W_apply' depends on axioms: [propext, Quot.sound]
'FRC.Fourier.J_apply' depends on axioms: [propext, Quot.sound]
'FRC.Fourier.pow_neg_val' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.J_sq' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.mul_J_apply' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.W_sq' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.W_mul_J_comm' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.natCast_card_pred_eq_neg_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.quarter_turn_sq' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.shell_relations' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.shell_relations_zmod' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.proj_mul_proj' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.sum_proj' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.frft_mul_proj_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.circle' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.rot_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.rot_cardinal' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.rot_eigenline' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.unitsEquivCircle' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.card_circle' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.gauss_mul_gauss_inv' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.gauss_inv_of_sign' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.shell_proj' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.shell_frft_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.shell_frft_cardinal' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.shell_frft_values' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.shell_frftLift' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.shell_conj' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.shell_frft_add_two_kappa' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.shell_heisenberg' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.shell_spectral_obstruction' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.shell_odd_proj_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.shell_even_proj_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.shell_frft_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.shell_multiplicity_sums' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.shell_multiplicity_tuple' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.p06012' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.p06014' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.p06016' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.p06017' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.p06018' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.p06019' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.p06021' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.p06022' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.p06023' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.p06025' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.p06031' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.p06032' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.p06034' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.p06035' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fourier.p06036' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Geometry.half_period' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Geometry.quarter_turn_order' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Geometry.orientation_class' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Geometry.euler_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Geometry.generator_orbit' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Geometry.principal_root' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Geometry.dft_inverse' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Geometry.euler_characteristic' depends on axioms: [propext, Quot.sound]
'FRC.Geometry.fixed_shell_gap' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Geometry.fixed_shell_gap_rat' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Geometry.fixed_shell_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Geometry.fixed_shell_bound_lt_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Geometry.p02007' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Geometry.p02010' depends on axioms: [propext, Quot.sound]
'FRC.Geometry.p02013' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Geometry.p02014' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Geometry.p02017' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Geometry.p02018' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Geometry.p02023' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Geometry.p02025' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Geometry.p02027' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Godel.finite_succ_onto' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Godel.infinite_of_succ' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Godel.theory_complete' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Godel.decTheory' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Godel.nots' does not depend on any axioms
'FRC.Godel.nots_injective' depends on axioms: [propext]
'FRC.Godel.no_goedel_numbering' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Godel.nots_collide' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Godel.no_injective_encoding' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Godel.reading_identifies' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Godel.alias_fibre' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Godel.alias_two' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Godel.alias_outside' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Godel.two_mul_catalan_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Godel.two_pow_le_catalan' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Godel.cohort_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Godel.abundance' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Godel.records_lt' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Godel.dense_coding' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Godel.decideAllRelations' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Godel.card_relations' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Godel.p25010' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Godel.p25011' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Godel.p25014' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Godel.p25015' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Godel.p25017' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Godel.p25019' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Godel.p25020' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Godel.p25048' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Godel.p25036' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.calibration_congruence' depends on axioms: [propext, Quot.sound]
'FRC.Gravity.newton_register' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.hbar_register' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.dilution' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.count_face' depends on axioms: [propext]
'FRC.Gravity.merger_area_law' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.cover_forcing' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.channel_q4' depends on axioms: [propext, Quot.sound]
'FRC.Gravity.operational_cut' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.photon_sphere' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.shadow_bracket' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.isco' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.isco_efficiency' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.capacity_ratio' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.capacity_ratio_numeral' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.redshift_linear' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.registration_root' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.crossover_limits' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.crossover_deep_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.crossover_newton_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.interpolant_discriminant' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.scale_invariance_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.dispersion_symbol' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.locked_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.exponential_reading' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.pn_series' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.preferred_frame_scale' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.dft' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.central_difference_adjoint' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.shift_theorem' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.tilt_bracket' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.floor_value' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.running_floor' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.p21001' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.p21009' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.p21016' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.p21017' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.p21019' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.p21020' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.p21022' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.p21023' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.p21024' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.p21026' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.p21027' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.p21062' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.p21030' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.p21031' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.p21033' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.p21064' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.p21035' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.p21040' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.p21042' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.p21048' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.p21049' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.p21050' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.p21060' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.p21051' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.p21052' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.p21053' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.p21054' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Gravity.p21055' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p00009' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p00133' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p00148' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p00192' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p00193' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p00201' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p14038' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p20032' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p20043' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p20044' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p20047' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p20080' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p21016' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p21019' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p21020' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p21022' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p21023' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p21026' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p21027' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p21030' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p21033' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p21042' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p21048' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p21049' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p21050' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p21051' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p21052' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p21053' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p21054' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p21055' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p21060' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p21062' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p21064' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p22005' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p22033' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p22035' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p22041' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p22050' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p22052' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p22054' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p22056' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p22061' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p26010' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p26011' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p26013' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p38010' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p38048' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p38049' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p03006' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p03007' depends on axioms: [propext, Quot.sound]
'FRC.LedgerML.p03009' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p03013' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p03014' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p06012' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p06014' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p06016' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p06017' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p06018' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p06019' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p06021' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p06022' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p06023' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p06025' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p06031' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p06032' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p06034' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p06035' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p06036' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p08011' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p21001' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p21009' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p21017' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p21024' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p21031' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p21035' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p21040' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p38022' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p38023' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p20008' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p20009' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p20011' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p20012' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p20013' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p20014' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p20015' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p20016' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p20017' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p05007' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p05009' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p05013' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p05019' depends on axioms: [propext]
'FRC.LedgerML.p22023' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p22024' depends on axioms: [propext]
'FRC.LedgerML.p22030' depends on axioms: [propext, Quot.sound]
'FRC.LedgerML.p22044' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.LedgerML.p22051' depends on axioms: [propext]
'FRC.LedgerML.p22053' depends on axioms: [propext]
'FRC.Pnp.gauss_product' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Pnp.gauss_modulus' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Pnp.family_bits' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Pnp.dilation_eigen' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Pnp.p26010' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Pnp.p26011' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Pnp.p26013' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Qm.sorkin_hierarchy' depends on axioms: [propext]
'FRC.Qm.gaussian_layers' depends on axioms: [propext]
'FRC.Qm.tsirelson_real' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Qm.ceiling_bracket' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Qm.pair_count_tally' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Qm.sorkin_second_witness' depends on axioms: [propext]
'FRC.Qm.tally_norm_eq' depends on axioms: [propext, Quot.sound]
'FRC.Qm.channel_entangles' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Qm.gaussian_minimal' depends on axioms: [propext, Quot.sound]
'FRC.Qm.gaussian_norm' depends on axioms: [propext, Quot.sound]
'FRC.Qm.singlet_law' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Qm.channel_chart' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Qm.omega_floors' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Qm.p22005' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Qm.p22023' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Qm.p22024' depends on axioms: [propext]
'FRC.Qm.p22030' depends on axioms: [propext, Quot.sound]
'FRC.Qm.p22033' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Qm.p22035' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Qm.p22041' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Qm.p22044' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Qm.p22050' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Qm.p22051' depends on axioms: [propext]
'FRC.Qm.p22052' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Qm.p22053' depends on axioms: [propext]
'FRC.Qm.p22054' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Qm.p22056' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Qm.p22061' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Reductio.certified_fraction_tendsto' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Reductio.finite_choice' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Reductio.periodic_choice' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Reductio.equivariant_section_iff' depends on axioms: [propext, Classical.choice]
'FRC.Reductio.obstruction_five' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Reductio.no_doubling' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Reductio.ultrafilter_principal' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Reductio.decideAllSubsets' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Reductio.nat_embeds' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Reductio.theory_complete' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Reductio.decRealize' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Reductio.decTheory' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Reductio.infinite_of_succ' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Reductio.cantor' does not depend on any axioms
'FRC.Reductio.cantor_finite' depends on axioms: [propext]
'FRC.Reductio.records_lt' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Reductio.no_mirror' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Reductio.p05007' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Reductio.p05009' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Reductio.p05013' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Reductio.p05014' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Reductio.p05019' depends on axioms: [propext]
'FRC.Reductio.p05024' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Reductio.p05027' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Reductio.p05028' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Reductio.p05029' depends on axioms: [propext, Classical.choice]
'FRC.Reductio.p05030' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Reductio.p05034' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Representation.Adequate' does not depend on any axioms
'FRC.Representation.adequate_inj' does not depend on any axioms
'FRC.Representation.transition_exists' depends on axioms: [Classical.choice, Quot.sound]
'FRC.Representation.transition_unique' depends on axioms: [Quot.sound]
'FRC.Representation.embeds_in_shell' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Representation.canonical_iota' depends on axioms: [Classical.choice, Quot.sound]
'FRC.Representation.chart_injective' does not depend on any axioms
'FRC.Representation.transition_images' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Representation.lift' depends on axioms: [Classical.choice, Quot.sound]
'FRC.Representation.consistency' depends on axioms: [Classical.choice, Quot.sound]
'FRC.Representation.sphere_of_equivariant' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Representation.godel_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Representation.mod_injective' depends on axioms: [propext]
'FRC.Representation.godel_instance' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Representation.p04008' does not depend on any axioms
'FRC.Representation.p04009' depends on axioms: [Classical.choice, Quot.sound]
'FRC.Representation.p04010' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Representation.p04011' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Representation.p04012' depends on axioms: [Classical.choice, Quot.sound]
'FRC.Representation.p04013' depends on axioms: [Classical.choice, Quot.sound]
'FRC.Representation.p04014' depends on axioms: [Classical.choice, Quot.sound]
'FRC.Representation.p04018' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Representation.p04020' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.zero_slot' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.slot_complementarity' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.ramanujan_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.half_turn' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.subject_constants' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.constants13' depends on axioms: [propext, Quot.sound]
'FRC.Rh.klein_four' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.fixed_frobenius' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.trace_eq_one_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.fixed_half_turn' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.norm_on_line' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.readout_on_line' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.card_critical_line' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.readout_slot_index' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.frobenius_eq_star' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.norm_eq_pow' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.phase_circle' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.quarter_turn_off_circle' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.scale_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.power_characters_not_orthonormal' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.character_eigen' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.chi_orthogonal' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.chi_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.chi_inversion' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.chi_parseval' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.flatness' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.vonMangoldt_moebius' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.zeros_in_strip' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.zero_of_sign_change' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.window_readback' depends on axioms: [propext, Quot.sound]
'FRC.Rh.prime_iff_window_irreducible' depends on axioms: [propext, Quot.sound]
'FRC.Rh.sqrt_sq_lt_prime' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.lab_pair' depends on axioms: [propext, Quot.sound]
'FRC.Rh.no_cycle_projection' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.p20008' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.p20009' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.p20011' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.p20012' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.p20013' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.p20014' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.p20015' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.p20016' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.p20017' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.p20080' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.p20032' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.p20043' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.p20044' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Rh.p20047' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.S13.ppn_faces' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.S13.registration_dictionary' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.S13.floor_value' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.S13.running_floor' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.S13.ladder_monotone' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.S13.p38010' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.S13.p38022' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.S13.p38023' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.S13.p38048' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.S13.p38049' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.scale_import' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.ln_omega_ledger' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.ceiling_bracket' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.omega_floors' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.zeta8' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.zeta8_pow_four' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.zeta8_inv' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.tsirelson_real' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.singlet_law' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.channel_chart' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.channel_entangles' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.family_bits' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.gauss_modulus' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.dilation_eigen' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.octant_chart' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.tanh_octant_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.age_rate_locus' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.lcdmAge' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.octant_inversion' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.tanh_eq_exp_two_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.exp_tail_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.exp_three_pi_four_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.tanh_octant_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.locus_bracket' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.locus_fine' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.landing_bracket' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.landing_fine' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.hubble_landing' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.hubble_stellar' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.floor_value' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.floor_fine' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.running_floor' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.ladder_monotone' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.tilt_ledger' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.efold_count' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.chi' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.coef' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.chi_conj' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.chi_orthogonal' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.chi_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.chi_inversion' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.chi_parseval' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.flatness' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.character_eigen' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.vonMangoldt_moebius' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.zero_re_nonpos_trivial' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.zeros_in_strip' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.line_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.line_ne_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.scale_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.completed_eq_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.completed_conj' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.completed_im_line' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.continuous_line_re' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Chart.zero_of_sign_change' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Extension.Ext.zero_re' does not depend on any axioms
'FRC.Extension.Ext.zero_im' does not depend on any axioms
'FRC.Extension.Ext.one_re' does not depend on any axioms
'FRC.Extension.Ext.one_im' does not depend on any axioms
'FRC.Extension.Ext.add_re' does not depend on any axioms
'FRC.Extension.Ext.add_im' does not depend on any axioms
'FRC.Extension.Ext.neg_re' depends on axioms: [propext]
'FRC.Extension.Ext.neg_im' depends on axioms: [propext]
'FRC.Extension.Ext.sub_re' does not depend on any axioms
'FRC.Extension.Ext.sub_im' does not depend on any axioms
'FRC.Extension.Ext.mul_re' does not depend on any axioms
'FRC.Extension.Ext.mul_im' does not depend on any axioms
'FRC.Extension.Ext.nsmul_re' does not depend on any axioms
'FRC.Extension.Ext.nsmul_im' does not depend on any axioms
'FRC.Extension.Ext.zsmul_re' does not depend on any axioms
'FRC.Extension.Ext.zsmul_im' does not depend on any axioms
'FRC.Extension.Ext.ofBase' does not depend on any axioms
'FRC.Extension.Ext.w' does not depend on any axioms
'FRC.Extension.Ext.conj' depends on axioms: [propext]
'FRC.Extension.Ext.norm' does not depend on any axioms
'FRC.Extension.Ext.ofBase_re' does not depend on any axioms
'FRC.Extension.Ext.ofBase_im' does not depend on any axioms
'FRC.Extension.Ext.w_re' does not depend on any axioms
'FRC.Extension.Ext.w_im' does not depend on any axioms
'FRC.Extension.Ext.conj_re' depends on axioms: [propext]
'FRC.Extension.Ext.conj_im' depends on axioms: [propext]
'FRC.Extension.Ext.w_sq' depends on axioms: [propext, Quot.sound]
'FRC.Extension.Ext.conj_mul' depends on axioms: [propext]
'FRC.Extension.Ext.conj_add' depends on axioms: [propext]
'FRC.Extension.Ext.conj_conj' depends on axioms: [propext]
'FRC.Extension.Ext.conj_one' depends on axioms: [propext]
'FRC.Extension.Ext.mul_conj' depends on axioms: [propext]
'FRC.Extension.Ext.norm_mul' depends on axioms: [propext, Quot.sound]
'FRC.Extension.Ext.ofBase_mul' depends on axioms: [propext]
'FRC.Extension.Ext.ofBase_add' depends on axioms: [propext]
'FRC.Extension.Ext.ofBase_one' does not depend on any axioms
'FRC.Extension.Ext.ofBase_zero' does not depend on any axioms
'FRC.Extension.Ext.ofBase_injective' does not depend on any axioms
'FRC.Extension.Ext.conj_ofBase' depends on axioms: [propext]
'FRC.Extension.Ext.conj_w' depends on axioms: [propext]
'FRC.Extension.Ext.conj_eq_self_iff' depends on axioms: [propext]
'FRC.Extension.Ext.conj_eq_neg_iff' depends on axioms: [propext]
'FRC.Extension.Ext.star_def' depends on axioms: [propext, Quot.sound]
'FRC.Extension.Ext.eq_re_add_im_w' depends on axioms: [propext]
'FRC.Extension.Ext.norm_eq_zero_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Extension.Ext.inv_def' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Extension.Ext.mul_inv_cancel'' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Extension.Ext.field' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Extension.no_causal_root' depends on axioms: [propext, Quot.sound]
'FRC.Extension.neg_sq_is_square' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Extension.absorb' depends on axioms: [propext, Quot.sound]
'FRC.Extension.aniso_tx' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Extension.boost_preserves' depends on axioms: [propext, Quot.sound]
'FRC.Extension.boost_comp' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Extension.boost_orthogonal' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Extension.gamma_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Extension.gamma_velocity' depends on axioms: [propext, Quot.sound]
'FRC.Extension.velocity_addition' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.DFT.sum_pow_eq_zero_of_ne_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.DFT.W' depends on axioms: [propext, Quot.sound]
'FRC.DFT.J' depends on axioms: [propext, Quot.sound]
'FRC.DFT.W_apply' depends on axioms: [propext, Quot.sound]
'FRC.DFT.J_apply' depends on axioms: [propext, Quot.sound]
'FRC.DFT.pow_neg_val' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.DFT.J_sq' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.DFT.mul_J_apply' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.DFT.W_sq' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.DFT.W_mul_J_comm' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.DFT.natCast_card_pred_eq_neg_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.DFT.quarter_turn_sq' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.DFT.shell_relations' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.DFT.shell_relations_zmod' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.chi' depends on axioms: [propext, Quot.sound]
'FRC.Fractional.chi_zero' depends on axioms: [propext, Quot.sound]
'FRC.Fractional.chi_add' depends on axioms: [propext, Quot.sound]
'FRC.Fractional.chi_mul_val' depends on axioms: [propext, Quot.sound]
'FRC.Fractional.chi_neg_add_self' depends on axioms: [propext, Quot.sound]
'FRC.Fractional.chi_ne_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.chi_pow_four' depends on axioms: [propext, Quot.sound]
'FRC.Fractional.sum_chi' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.phi' does not depend on any axioms
'FRC.Fractional.phi_zero' depends on axioms: [propext, Quot.sound]
'FRC.Fractional.phi_one' depends on axioms: [propext, Quot.sound]
'FRC.Fractional.phi_add' depends on axioms: [propext, Quot.sound]
'FRC.Fractional.proj' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.mul_proj' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.proj_mul_proj' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.sum_proj' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.pow_mul_proj' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.pow_eq_sum_proj' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.proj_eq_of_resolution' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.chi_pow_three' depends on axioms: [propext, Quot.sound]
'FRC.Fractional.proj_conj' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.psi' depends on axioms: [propext, Quot.sound]
'FRC.Fractional.psi_add' depends on axioms: [propext, Quot.sound]
'FRC.Fractional.psi_zero' depends on axioms: [propext, Quot.sound]
'FRC.Fractional.psi_nsmul' depends on axioms: [propext, Quot.sound]
'FRC.Fractional.frft' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.frft_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.frft_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.frft_nsmul' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.frft_cardinal' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.frft_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.frft_mul_proj_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.frftLift' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.frft_eq_frftLift' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.frftLift_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.frftLift_cardinal' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.frft_mul_proj' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.proj_mul_frft' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.cc' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.dd' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.rot' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.quarter_turn_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.inv_quarter_turn' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.circle' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.rot_det' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.rot_transpose_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.cc_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.dd_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.rot_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.rot_cardinal' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.rot_eigenline' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.Circle' depends on axioms: [propext, Quot.sound]
'FRC.Fractional.unitsEquivCircle' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.card_circle' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.psiF' depends on axioms: [propext, Quot.sound]
'FRC.Fractional.psiF_zero' depends on axioms: [propext, Quot.sound]
'FRC.Fractional.psiF_add' depends on axioms: [propext, Quot.sound]
'FRC.Fractional.psiF_mul_val' depends on axioms: [propext, Quot.sound]
'FRC.Fractional.psiF_neg_mul_self' depends on axioms: [propext, Quot.sound]
'FRC.Fractional.psiF_pow_n' depends on axioms: [propext, Quot.sound]
'FRC.Fractional.gauss' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.gauss_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.gauss_inv_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.two_mul_eq_zero_iff' depends on axioms: [propext, Quot.sound]
'FRC.Fractional.gauss_mul_gauss_inv' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.gauss_inv_of_sign' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.shift' depends on axioms: [propext, Quot.sound]
'FRC.Fractional.shift'' depends on axioms: [propext, Quot.sound]
'FRC.Fractional.modul' depends on axioms: [propext, Quot.sound]
'FRC.Fractional.shift_apply' depends on axioms: [propext, Quot.sound]
'FRC.Fractional.shift'_apply' depends on axioms: [propext, Quot.sound]
'FRC.Fractional.shift_mul_shift'' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.pow_succ_mod_mul' depends on axioms: [propext, Quot.sound]
'FRC.Fractional.val_add_one' depends on axioms: [propext]
'FRC.Fractional.W_mul_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.W_mul_modul' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.heisenberg' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.shift_mulVec_geom' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.frft_eigenvalue_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.rank_eq_trace_of_idempotent' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.natCast_four_mul_eq_neg_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.half_period' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.quarter_turn_sq'' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.quarter_turn_pow_four' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.two_ne_zero'' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.four_ne_zero'' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.inv_pow_kappa' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.inv_pow_four_kappa' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.chi_ne_one'' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.Fmat' depends on axioms: [propext, Quot.sound]
'FRC.Fractional.Fmat_sq' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.Fmat_pow_four' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.shellProj' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.shellFrft' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.shell_proj' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.shell_frft_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.shell_frft_cardinal' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.shell_frft_values' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.shell_frftLift' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.shell_conj' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.shell_frft_add_two_kappa' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.shell_heisenberg' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.shell_spectral_obstruction' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.sum_zmod_four' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.chi_values' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.parity_proj' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.J_mulVec_single' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.antisym_not_eigen' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.e0_not_eigen' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.shell_odd_proj_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.shell_even_proj_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.shell_frft_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.trace_Fmat' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.trace_J' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.four_mul_trace_proj' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.chi_neg_values' depends on axioms: [propext, Quot.sound]
'FRC.Fractional.four_mul_trace_proj_values' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.trace_proj_parity_sums' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.shell_multiplicity_dichotomy' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.rank_eq_of_trace_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.rank_add_of_orthogonal' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.card_zmod_shell' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.shell_multiplicity_sums' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Fractional.shell_multiplicity_tuple' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Frame.parity_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Frame.drive_nonsquare' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Frame.root_pair' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.GravML.calibration_congruence' depends on axioms: [propext, Quot.sound]
'FRC.GravML.newton_register' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.GravML.carrier_two_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.GravML.hbar_of_quarter_turn' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.GravML.hbar_register' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.GravML.count_face' depends on axioms: [propext]
'FRC.GravML.merger_area_law' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.GravML.cover_forcing' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.GravML.ppn_faces' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.GravML.registration_dictionary' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.GravML.channel_q4' depends on axioms: [propext, Quot.sound]
'FRC.GravML.central_difference_adjoint' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.GravML.dft' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.GravML.pow_val_mod' depends on axioms: [propext]
'FRC.GravML.pow_mul_val_mod' depends on axioms: [propext]
'FRC.GravML.shift_theorem' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.HorizonML.zero_slot' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.HorizonML.slot_complementarity' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.HorizonML.ramanujan_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.HorizonML.two_ne_zero_of_card' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.HorizonML.half_turn' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.HorizonML.half_period' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.HorizonML.subject_constants' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.HorizonML.constants13' depends on axioms: [propext, Quot.sound]
'FRC.HorizonML.trace_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.HorizonML.norm_eq' depends on axioms: [propext, Quot.sound]
'FRC.HorizonML.star_eq' depends on axioms: [propext, Quot.sound]
'FRC.HorizonML.klein_four' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.HorizonML.fixed_frobenius' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.HorizonML.trace_eq_one_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.HorizonML.fixed_half_turn' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.HorizonML.norm_on_line' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.HorizonML.readout' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.HorizonML.readout_on_line' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.HorizonML.card_critical_line' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.HorizonML.readout_slot_index' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.HorizonML.two_ne_zero_of_nonsquare' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.HorizonML.nonsquare_pow' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.HorizonML.frobenius_eq_star' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.HorizonML.norm_eq_pow' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.HorizonML.phase_circle' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.HorizonML.quarter_turn_off_circle' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.HorizonML.scale_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.HorizonML.power_characters_not_orthonormal' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.HorizonML.window_readback' depends on axioms: [propext, Quot.sound]
'FRC.HorizonML.prime_iff_window_irreducible' depends on axioms: [propext, Quot.sound]
'FRC.HorizonML.sqrt_sq_lt_prime' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.HorizonML.lab_pair' depends on axioms: [propext, Quot.sound]
'FRC.HorizonML.no_cycle_projection' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.HorizonML.gauss_product' depends on axioms: [propext, Classical.choice, Quot.sound]
'Bool.and' does not depend on any axioms
'FRC.Logic.theory_complete' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Logic.decRealize' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Logic.decTheory' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Logic.infinite_of_succ' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Logic.cantor' does not depend on any axioms
'FRC.Logic.cantor_finite' depends on axioms: [propext]
'FRC.Logic.records_lt' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Logic.no_mirror' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.QuantumML.mixedDiff' does not depend on any axioms
'FRC.QuantumML.sorkin_second' depends on axioms: [propext]
'FRC.QuantumML.sorkin_hierarchy' depends on axioms: [propext]
'FRC.QuantumML.sorkin_second_witness' depends on axioms: [propext]
'FRC.QuantumML.gi' does not depend on any axioms
'FRC.QuantumML.onePlusI' does not depend on any axioms
'FRC.QuantumML.onePlusI_sq' depends on axioms: [propext]
'FRC.QuantumML.gi_norm' does not depend on any axioms
'FRC.QuantumML.onePlusI_norm' does not depend on any axioms
'FRC.QuantumML.gaussian_layers' depends on axioms: [propext]
'FRC.QuantumML.norm_pow' depends on axioms: [propext, Quot.sound]
'FRC.QuantumML.gaussian_norm' depends on axioms: [propext, Quot.sound]
'FRC.QuantumML.gaussian_minimal' depends on axioms: [propext, Quot.sound]
'FRC.QuantumML.pair_count_tally' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.QuantumML.tally_norm_eq' depends on axioms: [propext, Quot.sound]
'FRC.Strong.dilution' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Strong.operational_cut' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Strong.photon_sphere' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Strong.sqrt_three_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Strong.shadow_bracket' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Strong.eikonal_pair' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Strong.isco' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Strong.exp_neg_bracket' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Strong.exp_isco_tail_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Strong.sqrt_five_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Strong.isco_efficiency' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Strong.capacity_ratio' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Strong.capacity_ratio_numeral' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Strong.redshift_linear' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Strong.registration_root' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Strong.crossover_limits' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Strong.crossover_deep_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Strong.crossover_newton_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Strong.exp_root_five_tail_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Strong.interpolant_discriminant' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Strong.scale_invariance_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Strong.dispersion_symbol' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Strong.locked_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Strong.exponential_reading' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Strong.pn_series' depends on axioms: [propext, Classical.choice, Quot.sound]
'FRC.Strong.preferred_frame_scale' depends on axioms: [propext, Classical.choice, Quot.sound]