'LatticeGaugeToeplitzTailSplit.split' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeToeplitzTailSplit.split_unique' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeToeplitzTailSplit.tail_sum_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeToeplitzTailSplit.tailPart_sum_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeToeplitzTailSplit.qform_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeToeplitzTailSplit.cform_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeToeplitzTailSplit.flatQ_two' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeToeplitzTailSplit.flat_row_sum_lt' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeToeplitzTailSplit.flatQ_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeToeplitzTailSplit.flat_not_uniform_geometric' depends on axioms: [propext, Classical.choice, Quot.sound]
