'LatticeGaugeHierarchicalUpperTube.tube_exit_of_lt' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeHierarchicalUpperTube.tube_exit_top' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeHierarchicalUpperTube.cell_descent' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeHierarchicalUpperTube.chain_top' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeHierarchicalUpperTube.steps_numeric_128' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeHierarchicalUpperTube.steps_numeric_64' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeHierarchicalUpperTube.mk_full_chain_128' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeHierarchicalUpperTube.union_tube_step' depends on axioms: [propext, Classical.choice, Quot.sound]
