diff --git a/logic_programming/7_Unification.ipynb b/logic_programming/7_Unification.ipynb
index 03e3dbc06fa955e834de63f294ff8275082039fc..3df2cc4ea203c183c07040bf5a4e6a9edb76da0c 100644
--- a/logic_programming/7_Unification.ipynb
+++ b/logic_programming/7_Unification.ipynb
@@ -13,19 +13,22 @@
     "\n",
     "### Substitutions\n",
     "\n",
-    "Substitution: mapping from variables to terms\n",
+    "A *substitution* is a mapping from variables to terms.\n",
+    "We use the following notation for substitutions:  {X1/t1, …, Xn/tn}\n",
     "\n",
-    "Notation:  {X1/t1, …, Xn/tn}\n",
-    "\n",
-    "Examples: \n",
+    "Examples of substitutions are: \n",
     "{X/a}  {X/b, Y/s(0)}  {Y/Z}  {}\n",
     "\n",
-    "In Prolog we represent this as lists of bindings:"
+    "Intuitively, ```{X/a}``` means we replace all occurences of X by a.\n",
+    "\n",
+    "In Prolog we represent substitutions as lists of bindings.\n",
+    "E.g., we represent ```{X/a}``` by ```['X'/a]``` where ```/``` is a functor of arity 2.\n",
+    "The following Prolog predicate checks is something is a valid substitution:"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": 50,
+   "execution_count": 1,
    "id": "78764141",
    "metadata": {
     "vscode": {
@@ -37,7 +40,7 @@
     "is_subst([]).\n",
     "is_subst([Var/Term|T]) :- variable(Var), term(Term), is_subst(T).\n",
     "\n",
-    "variable('$VAR'(_)).\n",
+    "variable('$VAR'(_)). % encode variables by this special functor\n",
     "variable('X'). % a few artificial variables for easier reading\n",
     "variable('Y').\n",
     "variable('Z').\n",
@@ -46,7 +49,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 14,
+   "execution_count": 2,
    "id": "b03ac6e7",
    "metadata": {
     "vscode": {
@@ -76,13 +79,14 @@
    "source": [
     "### Applying Substitutions\n",
     "\n",
-    "Applying a substitution to a term or wff\n",
-    "Instantaneous replacement by right-hand sides\n"
+    "Applying a substitution to a term or wff is done by\n",
+    "instantaneous and simultaneous replacement of all variables in the left-hand sides by the corresponding right-hand sides.\n",
+    "The following Prolog predicate applys a substitution to a term.\n"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": 12,
+   "execution_count": 3,
    "id": "f6f156a3",
    "metadata": {
     "vscode": {
@@ -105,7 +109,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 51,
+   "execution_count": 4,
    "id": "c675dc2a",
    "metadata": {
     "vscode": {
@@ -180,7 +184,7 @@
    "id": "c2f4b9a9",
    "metadata": {},
    "source": [
-    "A substitution s is called a unifier of two terms (or wff’s) A and B  iff  As = Bs\n"
+    "A substitution s is called a *unifier* of two terms (or wff’s) A and B  iff  As = Bs\n"
    ]
   },
   {