From 02cfe2a3041273042e188cc0046fd845046e49d2 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Fri, 29 May 2020 19:58:29 +0200
Subject: fix Pi congruence rule

---
 spartan/core/Spartan.thy | 4 ++--
 1 file 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"
-- 
cgit v1.2.3