Appending a singleton increases the list length

list_append_singleton_length

Submitter: Kim Morrison.

Notes: A simple list problem that exercises notation in generated files.

Source: Internal starter problem.

Informal solution: Compute the length after append.

theorem declaration uses `sorry`list_append_singleton_length :
    (([1, 2] : List Nat).append [3]).length = 3 := by⊢ ([1, 2].append [3]).length = 3
  sorryAll goals completed! 🐙

Solved by

• @rkirov with Claude Opus 4.7 on Apr 30, 2026 (proof)

• @kim-em with Aristotle (Harmonic) on May 1, 2026 (proof)