RetentionLesson.lean:40:43: warning: This simp argument is unused:
  Trace.length

Hint: Omit it from the simp argument list.
  simp [tick, net, Trace.step,̵ ̵T̵r̵a̵c̵e̵.̵l̵e̵n̵g̵t̵h̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
'ActualMathematics.RetentionLesson.tick_retains' depends on axioms: [propext, Quot.sound]
'ActualMathematics.RetentionLesson.record_counts_acts' depends on axioms: [propext, Quot.sound]
'ActualMathematics.RetentionLesson.record_append' depends on axioms: [propext, Quot.sound]
'ActualMathematics.RetentionLesson.count_join' depends on axioms: [propext, Quot.sound]
'ActualMathematics.RetentionLesson.net_join' depends on axioms: [propext, Quot.sound]
'ActualMathematics.RetentionLesson.backtrack' depends on axioms: [propext, Quot.sound]
'ActualMathematics.RetentionLesson.order_is_forgotten' does not depend on any axioms