/root/interactive/lean/phase3/NimRecurrent.lean:244:52: warning: This simp argument is unused:
  firstSome

Hint: Omit it from the simp argument list.
  simp only [hσ, hx, and_false, if_false, f̵i̵r̵s̵t̵S̵o̵m̵e̵,̵ ̵selFor, cancelIdx, ne_eq, not_false_eq_true,
  ̲  ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲true_and]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
/root/interactive/lean/phase3/NimRecurrent.lean:245:33: warning: This simp argument is unused:
  true_and

Hint: Omit it from the simp argument list.
  simp only [hσ, hx, and_false, if_false, firstSome, selFor, cancelIdx, ne_eq,
               ̵ ̵not_false_eq_true,̵ ̵t̵r̵u̵e̵_̵a̵n̵d̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
/root/interactive/lean/phase3/NimRecurrent.lean:253:35: warning: This simp argument is unused:
  firstSome

Hint: Omit it from the simp argument list.
  simp only [hx, if_false, f̵i̵r̵s̵t̵S̵o̵m̵e̵,̵ ̵decIdx]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
'NimAudit.Recurrent.run_append' depends on axioms: [propext]
'NimAudit.Recurrent.run_rows' depends on axioms: [propext, Quot.sound]
'NimAudit.Recurrent.run_position' depends on axioms: [propext, Quot.sound]
'NimAudit.Recurrent.fold_invariant' depends on axioms: [propext, Quot.sound]
'NimAudit.Recurrent.stream_from_init' depends on axioms: [propext, Quot.sound]
'NimAudit.Recurrent.serialize_empty' depends on axioms: [propext]
'NimAudit.Recurrent.consecutive_sep' depends on axioms: [propext, Quot.sound]
'NimAudit.Recurrent.sep_resets' depends on axioms: [propext]
'NimAudit.Recurrent.row_keeps' depends on axioms: [propext]
'NimAudit.Recurrent.step_width' depends on axioms: [propext, Quot.sound]
'NimAudit.Recurrent.run_width' depends on axioms: [propext, Quot.sound]
'NimAudit.Recurrent.stream_diff_one_heap' depends on axioms: [propext, Quot.sound]
'NimAudit.Recurrent.stream_restoration' depends on axioms: [propext, Quot.sound]
'NimAudit.Recurrent.stream_reports_delta' depends on axioms: [propext]
'NimAudit.Recurrent.shift_zero' depends on axioms: [propext, Quot.sound]
'NimAudit.Recurrent.firstSome_none_right' does not depend on any axioms
'NimAudit.Recurrent.shift_map_succ' depends on axioms: [propext, Quot.sound]
'NimAudit.Recurrent.replay_spec' depends on axioms: [propext, Quot.sound]
'NimAudit.Recurrent.replayMove_eq' depends on axioms: [propext, Quot.sound]
'NimAudit.Recurrent.terminal_nimSum_zero' depends on axioms: [propext, Quot.sound]
'NimAudit.Recurrent.replay_correct' depends on axioms: [propext, Quot.sound]
'NimAudit.Recurrent.two_scan_protocol' depends on axioms: [propext, Quot.sound]
'NimAudit.Recurrent.replay_resources' depends on axioms: [propext, Quot.sound]
'NimAudit.Recurrent.store_fold' depends on axioms: [propext, Quot.sound]
'NimAudit.Recurrent.store_fold0' depends on axioms: [propext, Quot.sound]
'NimAudit.Recurrent.store_correct' depends on axioms: [propext, Quot.sound]
'NimAudit.Recurrent.eval_xorC' depends on axioms: [propext, Quot.sound]
'NimAudit.Recurrent.enc_acc' depends on axioms: [propext]
'NimAudit.Recurrent.enc_prev' depends on axioms: [propext, Quot.sound]
'NimAudit.Recurrent.enc_valid' depends on axioms: [propext, Quot.sound]
'NimAudit.Recurrent.enc_tag' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Recurrent.enc_x' depends on axioms: [propext, Quot.sound]
'NimAudit.Recurrent.circuit_update' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Recurrent.ofBits_testBit_eq' depends on axioms: [propext, Quot.sound]
'NimAudit.Recurrent.circuit_step_correct' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.Recurrent.circuit_resources' depends on axioms: [propext, Quot.sound]
'NimAudit.Recurrent.xorNet_valid' depends on axioms: [propext, Quot.sound]
'NimAudit.Recurrent.xorNet_correct' does not depend on any axioms