'LatticeGaugeClassResidualTelescoping.telescoping_residual' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeClassResidualTelescoping.telescoping_residual_multi' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'LatticeGaugeClassResidualTelescoping.geometric_part_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeClassResidualTelescoping.inv_sq_step' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeClassResidualTelescoping.inv_sq_sum_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeClassResidualTelescoping.uniform_deviation' depends on axioms: [propext, Classical.choice, Quot.sound]

[exited with code 0]
