TreeGauge.lean:21: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`
'TreeGauge.treeGauge_root' depends on axioms: [propext, Quot.sound]
'TreeGauge.treeGauge_step' depends on axioms: [propext, Quot.sound]
'TreeGauge.treeGauge_trivializes' depends on axioms: [propext, Quot.sound]
'TreeGauge.exists_tree_gauge' depends on axioms: [propext, Quot.sound]
'TreeGauge.tree_gauge_unique' depends on axioms: [propext]
