From 76a8dd18161eca9b3c40502fac743f4cc3de3702 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Wed, 24 May 2017 17:12:26 -0400
Subject: [PATCH] fix(prod): revert change with unintended consequence

---
 hott/types/prod.hlean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/hott/types/prod.hlean b/hott/types/prod.hlean
index 38d33bed3..595e82881 100644
--- a/hott/types/prod.hlean
+++ b/hott/types/prod.hlean
@@ -22,7 +22,7 @@ namespace prod
   definition pair_eq [unfold 7 8] (pa : a = a') (pb : b = b') : (a, b) = (a', b') :=
   ap011 prod.mk pa pb
 
-  definition prod_eq [unfold 5 6] (H₁ : u.1 = v.1) (H₂ : u.2 = v.2) : u = v :=
+  definition prod_eq [unfold 3 4 5 6] (H₁ : u.1 = v.1) (H₂ : u.2 = v.2) : u = v :=
   by cases u; cases v; exact pair_eq H₁ H₂
 
   definition eq_pr1 [unfold 5] (p : u = v) : u.1 = v.1 :=