'LatticeGaugeHierarchicalTubeChain.tube_exit_of_lt' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeHierarchicalTubeChain.tube_exit' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeHierarchicalTubeChain.chain_compose' depends on axioms: [propext, Quot.sound]
'LatticeGaugeHierarchicalTubeChain.tube_weight_mono' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeHierarchicalTubeChain.cell_descent' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeHierarchicalTubeChain.mk_full_chain' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeHierarchicalTubeChain.steps_numeric' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeHierarchicalTubeChain.mk_full_chain_64' depends on axioms: [propext, Classical.choice, Quot.sound]
