aboutsummaryrefslogtreecommitdiff
path: root/spartan/core
diff options
context:
space:
mode:
authorJosh Chen2020-05-29 19:58:29 +0200
committerJosh Chen2020-05-29 19:58:29 +0200
commit02cfe2a3041273042e188cc0046fd845046e49d2 (patch)
tree3c80b9b11e00b3492b35d8b2ca6d400d15ca8254 /spartan/core
parent484988bc14c31710b8885aecb155ae120359c151 (diff)
fix Pi congruence rule
Diffstat (limited to 'spartan/core')
-rw-r--r--spartan/core/Spartan.thy4
1 files changed, 2 insertions, 2 deletions
diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index 3d59464..004ba8d 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -92,10 +92,10 @@ axiomatization where
eta: "f: \<Prod>x: A. B x \<Longrightarrow> \<lambda>x: A. f `x \<equiv> f" and
Pi_cong: "\<lbrakk>
+ \<And>x. x: A \<Longrightarrow> B x \<equiv> B' x;
A: U i;
\<And>x. x: A \<Longrightarrow> B x: U i;
- \<And>x. x: A \<Longrightarrow> B' x: U i;
- \<And>x. x: A \<Longrightarrow> B x \<equiv> B' x
+ \<And>x. x: A \<Longrightarrow> B' x: U i
\<rbrakk> \<Longrightarrow> \<Prod>x: A. B x \<equiv> \<Prod>x: A. B' x" and
lam_cong: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b x \<equiv> c x; A: U i\<rbrakk> \<Longrightarrow> \<lambda>x: A. b x \<equiv> \<lambda>x: A. c x"