diff --git a/HumanEvalLean/HumanEval5.lean b/HumanEvalLean/HumanEval5.lean
index be980d4..2450881 100644
--- a/HumanEvalLean/HumanEval5.lean
+++ b/HumanEvalLean/HumanEval5.lean
@@ -1,5 +1,49 @@
-def intersperse : Unit :=
-  ()
+example : [].intersperse 7 = []                              := rfl
+example : [5, 6, 3, 2].intersperse 8 = [5, 8, 6, 8, 3, 8, 2] := rfl
+example : [2, 2, 2].intersperse 2 = [2, 2, 2, 2, 2]          := rfl
+
+open List
+
+/--
+info: List.length_intersperse.{u_1} {α : Type u_1} {l : List α} {sep : α} : (intersperse sep l).length = 2 * l.length - 1
+-/
+#guard_msgs in
+#check length_intersperse
+
+/--
+info: List.getElem?_intersperse_two_mul.{u_1} {α : Type u_1} {l : List α} {sep : α} {i : Nat} :
+  (intersperse sep l)[2 * i]? = l[i]?
+-/
+#guard_msgs in
+#check getElem?_intersperse_two_mul
+
+/--
+info: List.getElem?_intersperse_two_mul_add_one.{u_1} {α : Type u_1} {l : List α} {sep : α} {i : Nat} (h : i + 1 < l.length) :
+  (intersperse sep l)[2 * i + 1]? = some sep
+-/
+#guard_msgs in
+#check getElem?_intersperse_two_mul_add_one
+
+/--
+info: List.getElem_intersperse_two_mul.{u_1} {α : Type u_1} {l : List α} {sep : α} {i : Nat}
+  (h : 2 * i < (intersperse sep l).length) : (intersperse sep l)[2 * i] = l[i]
+-/
+#guard_msgs in
+#check getElem_intersperse_two_mul
+
+/--
+info: List.getElem_intersperse_two_mul_add_one.{u_1} {α : Type u_1} {l : List α} {sep : α} {i : Nat}
+  (h : 2 * i + 1 < (intersperse sep l).length) : (intersperse sep l)[2 * i + 1] = sep
+-/
+#guard_msgs in
+#check getElem_intersperse_two_mul_add_one
+
+/--
+info: List.getElem_eq_getElem_intersperse_two_mul.{u_1} {α : Type u_1} {l : List α} {sep : α} {i : Nat} (h : i < l.length) :
+  l[i] = (intersperse sep l)[2 * i]
+-/
+#guard_msgs in
+#check getElem_eq_getElem_intersperse_two_mul
 
 /-!
 ## Prompt