diff --git a/susp_product.hlean b/susp_product.hlean
index 3de39d6..ad3d9a1 100644
--- a/susp_product.hlean
+++ b/susp_product.hlean
@@ -1,5 +1,5 @@
 import core
 open susp smash pointed wedge prod
 
-definition susp_product (X Y : Type*) : ⅀ (X × Y) ≃* ⅀ X ∨ (⅀ Y ∨ (X ∧ Y)) :=
+definition susp_product (X Y : Type*) : ⅀ (X × Y) ≃* ⅀ X ∨ (⅀ Y ∨ ⅀ (X ∧ Y)) :=
   sorry