diff --git a/HumanEvalLean/HumanEval28.lean b/HumanEvalLean/HumanEval28.lean
index 8f84ff6..970e9ce 100644
--- a/HumanEvalLean/HumanEval28.lean
+++ b/HumanEvalLean/HumanEval28.lean
@@ -1,7 +1,11 @@
 module
 
-def concatenate : Unit :=
-  ()
+def concatenate (strings : List String) : String :=
+  String.join strings
+
+theorem toList_concatenate {strings : List String} :
+    (concatenate strings).toList = strings.flatMap String.toList := by
+  simp [concatenate]
 
 /-!
 ## Prompt
@@ -41,4 +45,4 @@ def check(candidate):
     assert candidate(['x', 'y', 'z']) == 'xyz'
     assert candidate(['x', 'y', 'z', 'w', 'k']) == 'xyzwk'
 ```
--/
\ No newline at end of file
+-/