TreeGaugeLocality.lean:22:12: warning: Variable name `h` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _h

Note: This linter can be disabled with `set_option linter.unusedVariables false`
'TreeGaugeLocality.treeGauge_step' depends on axioms: [propext, Quot.sound]
'TreeGaugeLocality.gfix_tree_edge' depends on axioms: [propext, Quot.sound]
'TreeGaugeLocality.invariant_depends_on_nontree' depends on axioms: [propext, Classical.choice, Quot.sound]
