aboutsummaryrefslogtreecommitdiff
path: root/HoTT_Theorems.thy
diff options
context:
space:
mode:
Diffstat (limited to 'HoTT_Theorems.thy')
-rw-r--r--HoTT_Theorems.thy10
1 files changed, 5 insertions, 5 deletions
diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy
index 52e1b32..5578bf8 100644
--- a/HoTT_Theorems.thy
+++ b/HoTT_Theorems.thy
@@ -57,11 +57,11 @@ proposition wellformed_currying:
"B: A \<rightarrow> U" and
"\<And>x::Term. C(x): B(x) \<rightarrow> U"
shows "\<Prod>x:A. \<Prod>y:B(x). C x y : U"
-proof (rule Prod_formation)
+proof
fix x::Term
assume *: "x : A"
show "\<Prod>y:B(x). C x y : U"
- proof (rule Prod_formation)
+ proof
show "B(x) : U" using * by (rule assms)
qed (rule assms)
qed (rule assms)
@@ -78,15 +78,15 @@ proposition triply_curried:
"\<And>x y::Term. y : B(x) \<Longrightarrow> C(x)(y) : U" and
"\<And>x y z::Term. z : C(x)(y) \<Longrightarrow> D(x)(y)(z) : U"
shows "\<Prod>x:A. \<Prod>y:B(x). \<Prod>z:C(x)(y). D(x)(y)(z) : U"
-proof (rule Prod_formation)
+proof
fix x::Term assume 1: "x : A"
show "\<Prod>y:B(x). \<Prod>z:C(x)(y). D(x)(y)(z) : U"
- proof (rule Prod_formation)
+ proof
show "B(x) : U" using 1 by (rule assms)
fix y::Term assume 2: "y : B(x)"
show "\<Prod>z:C(x)(y). D(x)(y)(z) : U"
- proof (rule Prod_formation)
+ proof
show "C x y : U" using 2 by (rule assms)
show "\<And>z::Term. z : C(x)(y) \<Longrightarrow> D(x)(y)(z) : U" by (rule assms)
qed