From 3a34ca2b43fbd5725a7435dfafdb4cf179a8ec8b Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sat, 17 Apr 2021 17:16:45 +0100
Subject: Small fix: extraneous variable

---
 mltt/core/MLTT.thy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/mltt/core/MLTT.thy b/mltt/core/MLTT.thy
index 18bd2b7..19b9563 100644
--- a/mltt/core/MLTT.thy
+++ b/mltt/core/MLTT.thy
@@ -443,7 +443,7 @@ Lemma funcomp_lambda_comp [comp]:
 
 Lemma funcomp_apply_comp [comp]:
   assumes
-    "A: U i" "B: U i" "\<And>x y. x: B \<Longrightarrow> C x: U i"
+    "A: U i" "B: U i" "\<And>x. x: B \<Longrightarrow> C x: U i"
     "f: A \<rightarrow> B" "g: \<Prod>x: B. C x"
     "x: A"
   shows "(g \<circ>\<^bsub>A\<^esub> f) x \<equiv> g (f x)"
-- 
cgit v1.2.3