/root/interactive/lean/phase2/NimGame.lean:146:8: warning: unused variable `h`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
'NimAudit.Game.move_sum_lt' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.terminal_iff_no_move' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.terminal_lose' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.xor_eq_zero_imp' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.nimSum_move' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.move_from_zero' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.exists_move_to_zero' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.lose_of_zero_win_of_ne' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.not_win_and_lose' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.lose_iff' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.win_iff' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.wins_sound' does not depend on any axioms
'NimAudit.Game.testBit0_succ' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.rolloutWinner_eq' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.rolloutWinner_channel' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.ofBits_lt' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.testBit_ofBits' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.nimSum_lt' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.reconstruct_eq' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.cancelFirst_some' depends on axioms: [propext]
'NimAudit.Game.cancelFirst_none' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.cancelFirst_terminal' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.subFirstPos_terminal' depends on axioms: [propext]
'NimAudit.Game.selectMove_legal' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.selectMove_none_iff' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.selectMove_zero' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.width_move' depends on axioms: [propext]
'NimAudit.Game.agent_eq' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.agent_legal' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.agent_none_iff' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.agent_wins' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.agent_wins_of_win' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.agent_at_zero' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.agent_maintains' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.restore_correct' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.heapCount_le' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.rolloutMoves_le' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.totalRolloutMoves_le' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.nimSum_bits' depends on axioms: [propext]
'NimAudit.Game.nimSum_encode' depends on axioms: [propext]
'NimAudit.Game.nimSum_encode_ne' depends on axioms: [propext]
'NimAudit.Game.reduced_move' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.unique_zero_move' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.winning_selector_parity' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.agent_parity' depends on axioms: [propext, Quot.sound]
'NimAudit.Game.decode_reduced' does not depend on any axioms
'NimAudit.Game.no_winning_selector_of_hardness' depends on axioms: [propext, Quot.sound]