diff options
| -rw-r--r-- | spartan/core/Spartan.thy | 4 |
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" |