'HypothesisAlgebra.canonical_quartic' depends on axioms: [propext, Classical.choice, Quot.sound] 'HypothesisAlgebra.mass_coefficient' depends on axioms: [propext, Classical.choice, Quot.sound] 'HypothesisAlgebra.log_second_numerator' depends on axioms: [propext, Classical.choice, Quot.sound] 'HypothesisAlgebra.log_third_recurrence' depends on axioms: [propext, Classical.choice, Quot.sound] 'HypothesisAlgebra.log_fourth_recurrence' depends on axioms: [propext, Classical.choice, Quot.sound] 'HypothesisAlgebra.vacuum_offset_cancels' depends on axioms: [propext, Classical.choice, Quot.sound] 'HypothesisAlgebra.normalization_null_column' depends on axioms: [propext, Classical.choice, Quot.sound] 'HypothesisAlgebra.covariance_pullback_two' depends on axioms: [propext, Classical.choice, Quot.sound] 'HypothesisAlgebra.gram_minor_two' depends on axioms: [propext, Classical.choice, Quot.sound] 'HypothesisAlgebra.covariance_unit_minor' depends on axioms: [propext, Classical.choice, Quot.sound]