'CubicPathwidth.Alg.algoMixedNoFallback' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.Alg.algoMixedRealizesTheorem2b' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.Alg.algoMixedRealizesTheorem2c' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.Alg.algoMixedRealizesTheorem3P' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.Alg.algoMixedRealizesTheorem3R' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.Alg.algoMixedRealizesTheorem3S' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.Alg.algoMixedValid' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.Alg.algoMixedWidth' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.Alg.algoT1NoFallback' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.Alg.algoT1RealizesTheorem1' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.Alg.algoT1Valid' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.Alg.algoT1Width' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.Alg.algoT2aRealizesTheorem2a' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.Alg.algoT2aValid' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.Alg.algoT2aWidth' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.Alg.algoT4NoFallback' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.Alg.algoT4RealizesCorollary5' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.Alg.algoT4RealizesTheorem4' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.Alg.algoT4Valid' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.Alg.algoT4Width' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.Alg.connectorLemma10' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.Alg.connectorNoFallback' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.Alg.deletionProcessBound' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.Alg.undoNoFallback' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.Alg.undoWidth' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.C3.c3MainClaim' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.CutSweep.cutSweep' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.Locality.graph_correlation_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.PwSeq.targetBootstrapLemma' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.PwSeq.targetLemma2' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.PwSeq.targetRhoForm' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.PwSeq.targetThm1C' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.PwSeq.targetThm1F' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.PwSeq.targetThm1P' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.PwSeq.targetThm1R' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.PwSeq.targetThm1S' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.Sw4.targetThm1M' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.Sw4.targetThm62' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.T2.target2a' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.T2.target2b' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.T2.target2c' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.T3.target3P' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.T3.target3R' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.T3.target3S' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.T4.target4' depends on axioms: [propext, Classical.choice, Quot.sound]
'CubicPathwidth.T4.target5' depends on axioms: [propext, Classical.choice, Quot.sound]