'LatticeGaugeHierarchicalChainGeneral.tube_exit_of_lt' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeHierarchicalChainGeneral.tube_exit_top' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeHierarchicalChainGeneral.cell_descent' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeHierarchicalChainGeneral.chain_top' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeHierarchicalChainGeneral.mk_full_chain_general' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeHierarchicalChainGeneral.steps_general_at_128' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeHierarchicalChainGeneral.steps_general_mono' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeHierarchicalChainGeneral.steps_general_le_linear' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'LatticeGaugeHierarchicalChainGeneral.row_lt_req_of_columns' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeHierarchicalChainGeneral.uniform_columns' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeHierarchicalChainGeneral.uniform_columns_numeric' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'LatticeGaugeHierarchicalChainGeneral.uniform_columns_128' depends on axioms: [propext, Classical.choice, Quot.sound]
