From 1fd0ffe04dd9585ea17c8734e95e0f88cb5eadc0 Mon Sep 17 00:00:00 2001
From: Yiyun Liu <yliu8e5f7@protonmail.com>
Date: Fri, 27 Dec 2024 12:15:44 -0500
Subject: [PATCH] Minor

---
 theories/fp_red.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/fp_red.v b/theories/fp_red.v
index b3d73bb..33e8338 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -286,10 +286,10 @@ Module RPar.
   | ProjCong p a0 a1 :
     R a0 a1 ->
     R (Proj p a0) (Proj p a1)
-  | BindCong A0 A1 B0 B1:
+  | BindCong p A0 A1 B0 B1:
     R A0 A1 ->
     R B0 B1 ->
-    R (Pi A0 B0) (Pi A1 B1)
+    R (TBind p A0 B0) (TBind p A1 B1)
   | BotCong :
     R Bot Bot
   | UnivCong i :
@@ -404,10 +404,10 @@ Module EPar.
   | ProjCong p a0 a1 :
     R a0 a1 ->
     R (Proj p a0) (Proj p a1)
-  | BindCong A0 A1 B0 B1:
+  | BindCong p A0 A1 B0 B1:
     R A0 A1 ->
     R B0 B1 ->
-    R (Pi A0 B0) (Pi A1 B1)
+    R (TBind p A0 B0) (TBind p A1 B1)
   | BotCong :
     R Bot Bot
   | UnivCong i :