From df3ce3872fa11c394cb7918c157f0f631ac7bc1c Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Wed, 7 Jun 2017 09:38:33 -0600
Subject: [PATCH] Fix the statement of susp_product.

---
 susp_product.hlean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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