diff options
| author | Josh Chen | 2020-05-29 19:58:29 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-05-29 19:58:29 +0200 |
| commit | 02cfe2a3041273042e188cc0046fd845046e49d2 (patch) | |
| tree | 3c80b9b11e00b3492b35d8b2ca6d400d15ca8254 | |
| parent | 484988bc14c31710b8885aecb155ae120359c151 (diff) | |
fix Pi congruence rule
| -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" |