diff --git a/config.json b/config.json
index 03021ec..156f8f5 100644
--- a/config.json
+++ b/config.json
@@ -280,7 +280,6 @@
         "uuid": "367e9ad0-d3a1-403a-9c05-fc53a246c63b",
         "practices": [],
         "prerequisites": [],
-        "status": "wip",
         "difficulty": 3
       },
       {
diff --git a/exercises/practice/reverse-list/.docs/hints.md b/exercises/practice/reverse-list/.docs/hints.md
new file mode 100644
index 0000000..696dcd1
--- /dev/null
+++ b/exercises/practice/reverse-list/.docs/hints.md
@@ -0,0 +1,23 @@
+## General
+
+- The tactic [`funext`][funext] can reduce a proof of equality between functions to proving that they return the same value for all possible arguments.
+It introduces a new argument into the proof, representing an input applied to both functions.
+
+- Using `@` before a function makes all [implicit parameters][implicit-parameters] explicit.
+That means type variables can be brought into scope with `funext`.
+
+- The [`induction` tactic][induction-tactic] is often useful for constructing proofs by [mathematical induction][mathematical-induction] on inductive types.
+
+- Simplification tactics such as [`simp`][simp] may help after applying induction.
+
+- There are many `List` lemmas that can serve as a starting point for your proof.
+They are listed in the [API reference][api-reference], particularly in [Init.Data.List.Basic][list-basic] and [Init.Data.List.Lemmas][list-lemmas].
+
+[funext]: https://lean-lang.org/doc/reference/latest/Tactic-Proofs/Tactic-Reference/#funext-next
+[implicit-parameters]: https://lean-lang.org/doc/reference/latest/Terms/Functions/#implicit-functions
+[induction-tactic]: https://lean-lang.org/doc/reference/latest/Tactic-Proofs/Tactic-Reference/#induction
+[mathematical-induction]: https://en.wikipedia.org/wiki/Mathematical_induction
+[simp]: https://lean-lang.org/doc/reference/4.19.0//Tactic-Proofs/Tactic-Reference/#simp
+[api-reference]: https://lean-lang.org/doc/api/
+[list-basic]: https://lean-lang.org/doc/api/Init/Data/List/Basic.html
+[list-lemmas]: https://lean-lang.org/doc/api/Init/Data/List/Lemmas.html
diff --git a/exercises/practice/reverse-list/.docs/instructions.append.md b/exercises/practice/reverse-list/.docs/instructions.append.md
new file mode 100644
index 0000000..967f3eb
--- /dev/null
+++ b/exercises/practice/reverse-list/.docs/instructions.append.md
@@ -0,0 +1,33 @@
+# Instructions append
+
+## Proving theorems in Lean
+
+Theorem proving is an integral part of Lean.
+It empowers programmers to prove properties about their programs, reason about their behavior, and encode constraints and specifications at the type level.
+
+[This chapter][introduction] provides a good introduction to theorem proving in Lean.
+For a deeper dive, [this book][advanced] is listed as an official resource on the Lean website.
+
+Lean offers many tactics that can automate proofs, or parts of them. 
+You might want to check a [language reference][reference].
+
+~~~~exercism/advanced
+We can use the compiler attribute `csimp` on a theorem proving equality between two definitions.
+This attribute instructs the compiler to use the second definition in place of the first:
+
+```lean
+@[csimp]
+theorem custom_reverse_eq_spec_reverse : @Extra.custom_reverse = @List.reverse := by
+    ... -- proof here
+
+-- now any occurrence of `Extra.custom_reverse` may now compile to `List.reverse`.
+```
+
+It is particularly useful in situations where an implementation is more efficient but less clear.
+We can write a simple specification and have compiled code use the more efficient implementation instead.
+Many `List` and `Array` functions use this pattern.
+~~~~
+
+[introduction]: https://lean-lang.org/functional_programming_in_lean/Programming___-Proving___-and-Performance/
+[advanced]: https://lean-lang.org/theorem_proving_in_lean4/
+[reference]: https://lean-lang.org/doc/reference/latest/Tactic-Proofs/#tactics
diff --git a/exercises/practice/reverse-list/.docs/instructions.md b/exercises/practice/reverse-list/.docs/instructions.md
index b46948a..a33de52 100644
--- a/exercises/practice/reverse-list/.docs/instructions.md
+++ b/exercises/practice/reverse-list/.docs/instructions.md
@@ -14,4 +14,4 @@ It is an invaluable tool, capable of showing all local values in use by your pro
 The `sorry` tactic makes any proof appear to be correct. 
 For this reason, the `check` theorem might appear to automatically typecheck before any proof is actually written.
 Once you remove `sorry` from your proof, Lean InfoView will show the correct feedback.
-~~~~
\ No newline at end of file
+~~~~
diff --git a/exercises/practice/reverse-list/.meta/Example.lean b/exercises/practice/reverse-list/.meta/Example.lean
index 11363b4..21a7314 100644
--- a/exercises/practice/reverse-list/.meta/Example.lean
+++ b/exercises/practice/reverse-list/.meta/Example.lean
@@ -1,13 +1,13 @@
-import Spec
+import Extra
 
 namespace ReverseList
 
 @[csimp]
-theorem custom_reverse_eq_spec_reverse : @Spec.custom_reverse = @List.reverse := by
+theorem custom_reverse_eq_spec_reverse : @Extra.custom_reverse = @List.reverse := by
   funext α
   funext xs
   induction xs with
   | nil         => rfl
-  | cons x xs' ir => simpa [Spec.custom_reverse, List.reverse_cons] using ir
+  | cons x xs' ir => simpa [Extra.custom_reverse, List.reverse_cons] using ir
 
 end ReverseList
diff --git a/exercises/practice/reverse-list/.meta/config.json b/exercises/practice/reverse-list/.meta/config.json
index 4eaa5f8..3e73578 100644
--- a/exercises/practice/reverse-list/.meta/config.json
+++ b/exercises/practice/reverse-list/.meta/config.json
@@ -13,9 +13,9 @@
       ".meta/Example.lean"
     ],
     "editor": [
-      "Spec.lean"
+      "Extra.lean"
     ]
   },
   "icon": "array-loops",
-  "blurb": "Prove equality between a custom function and the built-in List.reverse function."
+  "blurb": "Prove the equality between a custom function and the built-in List.reverse."
 }
diff --git a/exercises/practice/reverse-list/Spec.lean b/exercises/practice/reverse-list/Extra.lean
similarity index 81%
rename from exercises/practice/reverse-list/Spec.lean
rename to exercises/practice/reverse-list/Extra.lean
index 3f744c6..796e687 100644
--- a/exercises/practice/reverse-list/Spec.lean
+++ b/exercises/practice/reverse-list/Extra.lean
@@ -1,7 +1,7 @@
-namespace Spec
+namespace Extra
 
 def custom_reverse {α : Type u} : List α → List α
   | []      => []
   | x :: xs => custom_reverse xs ++ [x]
 
-end Spec
+end Extra
diff --git a/exercises/practice/reverse-list/ReverseList.lean b/exercises/practice/reverse-list/ReverseList.lean
index b68ebd6..3955881 100644
--- a/exercises/practice/reverse-list/ReverseList.lean
+++ b/exercises/practice/reverse-list/ReverseList.lean
@@ -1,9 +1,9 @@
-import Spec
+import Extra
 
 namespace ReverseList
 
 @[csimp]
-theorem custom_reverse_eq_spec_reverse: @Spec.custom_reverse = @List.reverse := by
+theorem custom_reverse_eq_spec_reverse: @Extra.custom_reverse = @List.reverse := by
   sorry --remove this line and implement the proof
 
 end ReverseList
diff --git a/exercises/practice/reverse-list/ReverseListTest.lean b/exercises/practice/reverse-list/ReverseListTest.lean
index 33c6461..304b052 100644
--- a/exercises/practice/reverse-list/ReverseListTest.lean
+++ b/exercises/practice/reverse-list/ReverseListTest.lean
@@ -1,9 +1,10 @@
 import LeanTest
 import ReverseList
+import Extra
 
 open LeanTest
 
-theorem check: @Spec.custom_reverse = @List.reverse := by
+theorem check: @Extra.custom_reverse = @List.reverse := by
   exact ReverseList.custom_reverse_eq_spec_reverse
 
 def main : IO UInt32 := do
diff --git a/exercises/practice/reverse-list/lakefile.toml b/exercises/practice/reverse-list/lakefile.toml
index b87eafd..7d05e5b 100644
--- a/exercises/practice/reverse-list/lakefile.toml
+++ b/exercises/practice/reverse-list/lakefile.toml
@@ -12,7 +12,7 @@ srcDir = "vendor/LeanTest"
 name = "ReverseList"
 
 [[lean_lib]]
-name = "Spec"
+name = "Extra"
 
 [[lean_exe]]
 name = "ReverseListTest"
diff --git a/generators/Generator/Generator/ReverseListGenerator.lean b/generators/Generator/Generator/ReverseListGenerator.lean
index ee867d1..adbb74b 100644
--- a/generators/Generator/Generator/ReverseListGenerator.lean
+++ b/generators/Generator/Generator/ReverseListGenerator.lean
@@ -10,10 +10,11 @@ namespace ReverseListGenerator
 
 def genIntro (exercise : String) : String := s!"import LeanTest
 import {exercise}
+import Extra
 
 open LeanTest
 
-theorem check: @Spec.custom_reverse = @List.reverse := by
+theorem check: @Extra.custom_reverse = @List.reverse := by
   exact {exercise}.custom_reverse_eq_spec_reverse"
 
 def genTestCase (_exercise : String) (_case : TreeMap.Raw String Json) : String := ""