From 2fe0d3359234a9c51d65a7eaef0fca41797f58b3 Mon Sep 17 00:00:00 2001
From: Yiyun Liu <yliu8e5f7@protonmail.com>
Date: Sun, 29 Dec 2024 22:36:15 -0500
Subject: [PATCH] Minor

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

diff --git a/theories/logrel.v b/theories/logrel.v
index d707dfd..af9d144 100644
--- a/theories/logrel.v
+++ b/theories/logrel.v
@@ -15,7 +15,7 @@ Inductive InterpExt {n} i (I : forall n, nat -> Tm n -> Prop) : Tm n -> (Tm n ->
   ⟦ A ⟧ i ;; I ↘ PA ->
   (forall a, PA a -> exists PB, PF a PB) ->
   (forall a PB, PF a PB -> ⟦ subst_Tm (scons a VarTm) B ⟧ i ;; I ↘ PB) ->
-  ⟦ Pi A B ⟧ i ;; I ↘ (ProdSpace PA PF)
+  ⟦ TBind TPi A B ⟧ i ;; I ↘ (ProdSpace PA PF)
 
 | InterpExt_Univ j :
   j < i ->
@@ -86,19 +86,19 @@ Lemma RPar_substone n (a b : Tm (S n)) (c : Tm n):
   Proof. hauto l:on inv:option use:RPar.substing, RPar.refl. Qed.
 
 Lemma InterpExt_Fun_inv n i I (A : Tm n) B P
-  (h :  ⟦ Pi A B ⟧ i ;; I ↘ P) :
+  (h :  ⟦ TBind TPi A B ⟧ i ;; I ↘ P) :
   exists (PA : Tm n -> Prop) (PF : Tm n -> (Tm n -> Prop) -> Prop),
      ⟦ A ⟧ i ;; I ↘ PA /\
     (forall a, PA a -> exists PB, PF a PB) /\
     (forall a PB, PF a PB -> ⟦ subst_Tm (scons a VarTm) B ⟧ i ;; I ↘ PB) /\
     P = ProdSpace PA PF.
 Proof.
-  move E : (Pi A B) h => T h.
+  move E : (TBind TPi A B) h => T h.
   move : A B E.
   elim : T P / h => //.
   - hauto l:on.
   - move => A A0 PA hA hA0 hPi A1 B ?. subst.
-    elim /RPar.inv : hA => //= _ A2 A3 B0 B1 hA1 hB0 [*]. subst.
+    elim /RPar.inv : hA => //= _ p A2 A3 B0 B1 hA1 hB0 [*]. subst.
     hauto lq:on ctrs:InterpExt use:RPar_substone.
 Qed.