/-- List benchmark: appending an empty list on the right is identity. -/
theorem list_append_nil_nat (xs : List Nat) : xs ++ [] = xs := by
{{PROOF}}