diff --git a/index.md b/index.md
index 3d16aea2..b4892d0b 100644
--- a/index.md
+++ b/index.md
@@ -59,8 +59,12 @@ Pull requests are encouraged.
     * Prabhakar Ragde, University of Waterloo,
 	  [2019](https://cs.uwaterloo.ca/~plragde/842/)
   - A paper describing the book appeared in [SBMF][sbmf].
-
+  - A notebook version of the textbook
+    is available at [NextJournal][nextjournal].
+    It lets you edit and execute the book via a web interface.
+	
 [wen]: https://github.com/wenkokke
 [phil]: https://homepages.inf.ed.ac.uk/wadler/
 [GitHub]: https://github.com/plfa/plfa.github.io/
 [sbmf]: https://homepages.inf.ed.ac.uk/wadler/topics/agda.html#sbmf
+[nextjournal]: https://nextjournal.com/plfa/ToC
diff --git a/src/plfa/part1/Lists.lagda.md b/src/plfa/part1/Lists.lagda.md
index 56cd7816..e70592c0 100644
--- a/src/plfa/part1/Lists.lagda.md
+++ b/src/plfa/part1/Lists.lagda.md
@@ -354,6 +354,30 @@ reverse of the second appended to the reverse of the first:
 
     reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
 
+
+```
+reverse-++-distrib : ∀ xs ys → reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
+reverse-++-distrib [] ys = 
+  begin
+    reverse ([] ++ ys)
+  ≡⟨⟩
+    reverse ys
+  ≡⟨ sym (++-identityʳ (reverse ys)) ⟩
+    reverse ys ++ reverse []
+  ∎
+reverse-++-distrib (x ∷ xs) ys =
+  begin
+    reverse ((x ∷ xs) ++ ys)
+  ≡⟨⟩
+    reverse (xs ++ ys) ++ [ x ]
+  ≡⟨ cong (_++ [ x ]) (reverse-++-distrib xs ys) ⟩
+    (reverse ys ++ reverse xs) ++ [ x ]
+  ≡⟨ ++-assoc (reverse ys) (reverse xs) [ x ] ⟩
+    reverse ys ++ (reverse xs ++ [ x ])
+  ∎
+```
+
+
 #### Exercise `reverse-involutive` (recommended)
 
 A function is an _involution_ if when applied twice it acts