X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fpr3%2Ffwd.ma;h=726c420f002cf13e64e15d03e34705f56c46e75d;hb=fc8408a10c29e472ec05e725a36da1f71d850937;hp=258df5e4c755559bb002111534b36c32dc7d31a3;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr3/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr3/fwd.ma
index 258df5e4c..726c420f0 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr3/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr3/fwd.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/pr3/props.ma".
+include "Basic-1/pr3/props.ma".
 
-include "LambdaDelta-1/pr2/fwd.ma".
+include "Basic-1/pr2/fwd.ma".
 
 theorem pr3_gen_sort:
  \forall (c: C).(\forall (x: T).(\forall (n: nat).((pr3 c (TSort n) x) \to 
@@ -34,6 +34,9 @@ t2)))).(\lambda (H4: (eq T t1 (TSort n))).(let H5 \def (eq_ind T t1 (\lambda
 T).(eq T t3 t)) (let H6 \def (eq_ind T t2 (\lambda (t: T).((eq T t (TSort n)) 
 \to (eq T t3 t))) H3 (TSort n) (pr2_gen_sort c t2 n H5)) in (H6 (refl_equal T 
 (TSort n)))) t1 H4))))))))) y x H0))) H)))).
+(* COMMENTS
+Initial nodes: 253
+END *)
 
 theorem pr3_gen_abst:
  \forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr3 c 
@@ -107,6 +110,9 @@ B).(\forall (u: T).(pr3 (CHead c (Bind b) u) x3 x5))))).(ex3_2_intro T T
 x4 x5 H12 (pr3_sing c x2 x0 H8 x4 H13) (\lambda (b: B).(\lambda (u: 
 T).(pr3_sing (CHead c (Bind b) u) x3 x1 (H9 b u) x5 (H14 b u)))))))))) 
 H11)))))))) H6)))))))))))) y x H0))))) H))))).
+(* COMMENTS
+Initial nodes: 1261
+END *)
 
 theorem pr3_gen_cast:
  \forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr3 c 
@@ -209,6 +215,9 @@ x3 x1 H10 t4 H13))) H12)))))))) H7)) (\lambda (H7: (pr2 c x1 t2)).(or_intror
 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: 
 T).(\lambda (t5: T).(pr3 c x1 t5)))) (pr3 c x1 t4) (pr3_sing c t2 x1 H7 t4 
 H2))) H6)))))))))))) y x H0))))) H))))).
+(* COMMENTS
+Initial nodes: 2001
+END *)
 
 theorem pr3_gen_lift:
  \forall (c: C).(\forall (t1: T).(\forall (x: T).(\forall (h: nat).(\forall 
@@ -246,6 +255,9 @@ h d t5))) (\lambda (t5: T).(pr3 e x1 t5)) (ex2 T (\lambda (t5: T).(eq T t4
 (\lambda (t5: T).(eq T t4 (lift h d t5))) (\lambda (t5: T).(pr3 e x0 t5)) x2 
 H10 (pr3_sing e x1 x0 H9 x2 H11))))) (H3 x1 H8 e H5))))) H7))))))))))))) y x 
 H0)))) H)))))).
+(* COMMENTS
+Initial nodes: 689
+END *)
 
 theorem pr3_gen_lref:
  \forall (c: C).(\forall (x: T).(\forall (n: nat).((pr3 c (TLRef n) x) \to 
@@ -324,6 +336,9 @@ T).(\lambda (_: T).(getl n c (CHead d (Bind Abbr) u))))) (\lambda (d:
 C).(\lambda (u: T).(\lambda (v: T).(pr3 d u v)))) (\lambda (_: C).(\lambda 
 (_: T).(\lambda (v: T).(eq T t3 (lift (S n) O v))))) x0 x1 x2 H8 H14 H13))))) 
 H12)))))))) H7)) H6)) t1 H4))))))))) y x H0))) H)))).
+(* COMMENTS
+Initial nodes: 1515
+END *)
 
 theorem pr3_gen_void:
  \forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr3 c 
@@ -454,6 +469,9 @@ c (Bind b) u) x1 t5)))))) (pr3 (CHead c (Bind Void) x0) x1 (lift (S O) O t4))
 (pr3_sing (CHead c (Bind Void) x0) (lift (S O) O t2) x1 (H7 Void x0) (lift (S 
 O) O t4) (pr3_lift (CHead c (Bind Void) x0) c (S O) O (drop_drop (Bind Void) 
 O c c (drop_refl c) x0) t2 t4 H2)))) H6)))))))))))) y x H0))))) H))))).
+(* COMMENTS
+Initial nodes: 2645
+END *)
 
 theorem pr3_gen_abbr:
  \forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr3 c 
@@ -721,6 +739,9 @@ x0) x1 t5)))) (pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)) (pr3_sing
 (CHead c (Bind Abbr) x0) (lift (S O) O t2) x1 (H7 Abbr x0) (lift (S O) O t4) 
 (pr3_lift (CHead c (Bind Abbr) x0) c (S O) O (drop_drop (Bind Abbr) O c c 
 (drop_refl c) x0) t2 t4 H2)))) H6)))))))))))) y x H0))))) H))))).
+(* COMMENTS
+Initial nodes: 5983
+END *)
 
 theorem pr3_gen_appl:
  \forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr3 c 
@@ -1486,6 +1507,9 @@ T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(pr3 (CHead c (Bind b)
 y2) z1 z2))))))) x2 x3 x4 x5 x6 x7 H8 (pr3_refl c (THead (Bind x2) x3 x4)) 
 H15 (pr3_pr2 c x0 x6 H11) (pr3_pr2 c x3 x7 H12) (pr3_pr2 (CHead c (Bind x2) 
 x7) x4 x5 H13))))) x1 H9))))))))))))) H7)) H6)))))))))))) y x H0))))) H))))).
+(* COMMENTS
+Initial nodes: 12691
+END *)
 
 theorem pr3_gen_bind:
  \forall (b: B).((not (eq B b Abst)) \to (\forall (c: C).(\forall (u1: 
@@ -1574,4 +1598,7 @@ H3 H4 (H5 Void u1)))))))) H2)) (\lambda (H2: (pr3 (CHead c (Bind Void) u1) t1
 T).(eq T x (THead (Bind Void) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3 
 c u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr3 (CHead c (Bind Void) u1) t1 
 t2)))) (pr3 (CHead c (Bind Void) u1) t1 (lift (S O) O x)) H2)) H1)))))))) b).
+(* COMMENTS
+Initial nodes: 1721
+END *)