From e5a48ef62fd66ffc1b36d82eedb5663f25c1a9a3 Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Sun, 2 Feb 2020 13:36:53 +0100
Subject: [PATCH] typable lhs

---
 encodings/cert_f.lp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/encodings/cert_f.lp b/encodings/cert_f.lp
index ef6370d..328af9d 100644
--- a/encodings/cert_f.lp
+++ b/encodings/cert_f.lp
@@ -31,7 +31,7 @@ rule Term uProp → Univ Prop
 symbol prod {s1 s2 : Sort} (A : Univ s1) :
   (Term A ⇒ Univ s2) ⇒ Univ (Rule s1 s2)
 
-rule Term (prod &A &B) → ∀ x : Term &A, Term (&B x)
+rule Term (@prod &s1 &s2 &A &B) → ∀ x : @Term &s1 &A, @Term &s2 (&B x)
 
 // Predicate subtyping
 // can be seen as a dependant pair type with
-- 
GitLab