diff --git a/docusaurus-site/docs/lectures/L1.mdx b/docusaurus-site/docs/lectures/L1.mdx
index e3df2b8..3cb8f00 100644
--- a/docusaurus-site/docs/lectures/L1.mdx
+++ b/docusaurus-site/docs/lectures/L1.mdx
@@ -44,20 +44,20 @@ in a group “<span class="purpbold">assuming</span> that $x^2=1$ for all $x$, p
 
 ```tptp
 %---- 1 * x = x
-fof(left identity,axiom,
+fof(left_identity,axiom,
 ! [X] : mult(e,X) = X).
 %---- i(x) * x = 1
-fof(left inverse,axiom,
+fof(left_inverse,axiom,
 ! [X] : mult(inverse(X),X) = e).
 %---- (x * y) * z = x * (y * z)
 fof(associativity,axiom,
 ! [X,Y,Z] : mult(mult(X,Y),Z) = mult(X,mult(Y,Z))).
 %---- x * x = 1
-fof(group of order 2,hypothesis,
+fof(group_of_order_2,hypothesis,
 ! [X] : mult(X,X) = e).
 %---- prove x * y = y * x
 fof(commutativity,conjecture,
-! [X] : mult(X,Y) = mult(Y,X)).
+! [X, Y] : mult(X,Y) = mult(Y,X)).
 ```
 
 ## First-Order Logic and TPTP