X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fpr0%2Ffwd.ma;h=46caceab4fb19492e138f6dc1000d4bc3a3a67c0;hb=bf8fe5331d6e6d2dfe955efa54b1ffdafaae8429;hp=7ad8f8eef4b91e477625c9ad3f158224428075f8;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr0/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr0/fwd.ma
index 7ad8f8eef..46caceab4 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr0/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr0/fwd.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/pr0/props.ma".
+include "Basic-1/pr0/props.ma".
 
 theorem pr0_gen_sort:
  \forall (x: T).(\forall (n: nat).((pr0 (TSort n) x) \to (eq T x (TSort n))))
@@ -77,6 +77,9 @@ T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
 False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I 
 (TSort n) H3) in (False_ind (eq T t2 (THead (Flat Cast) u t1)) H4)))))))) y x 
 H0))) H))).
+(* COMMENTS
+Initial nodes: 1045
+END *)
 
 theorem pr0_gen_lref:
  \forall (x: T).(\forall (n: nat).((pr0 (TLRef n) x) \to (eq T x (TLRef n))))
@@ -139,6 +142,9 @@ T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
 False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I 
 (TLRef n) H3) in (False_ind (eq T t2 (THead (Flat Cast) u t1)) H4)))))))) y x 
 H0))) H))).
+(* COMMENTS
+Initial nodes: 1045
+END *)
 
 theorem pr0_gen_abst:
  \forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr0 (THead (Bind Abst) u1 
@@ -311,6 +317,9 @@ _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _)
 t1) H3) in (False_ind (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 
 (THead (Bind Abst) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) 
 (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3)))) H4)))))))) y x H0))) H)))).
+(* COMMENTS
+Initial nodes: 2838
+END *)
 
 theorem pr0_gen_appl:
  \forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr0 (THead (Flat Appl) u1 
@@ -1082,6 +1091,9 @@ u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
 T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1 v2))))))) (\lambda (_: 
 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda 
 (t3: T).(pr0 z1 t3))))))))) H4)))))))) y x H0))) H)))).
+(* COMMENTS
+Initial nodes: 12299
+END *)
 
 theorem pr0_gen_cast:
  \forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr0 (THead (Flat Cast) u1 
@@ -1248,6 +1260,9 @@ T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1 t2)))) H2 t1 H5) in (let H8 \def
 (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Flat Cast) u2 t3)))) 
 (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3: 
 T).(pr0 t1 t3)))) (pr0 t1 t2) H8))))) H4)))))))) y x H0))) H)))).
+(* COMMENTS
+Initial nodes: 2911
+END *)
 
 theorem pr0_gen_abbr:
  \forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr0 (THead (Bind Abbr) u1 
@@ -1492,6 +1507,9 @@ u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (u2:
 T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) 
 (\lambda (y0: T).(subst0 O u2 y0 t3))))))) (pr0 t1 (lift (S O) O t2))) 
 H4)))))))) y x H0))) H)))).
+(* COMMENTS
+Initial nodes: 4711
+END *)
 
 theorem pr0_gen_void:
  \forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr0 (THead (Bind Void) u1 
@@ -1681,6 +1699,9 @@ t2)))))).(\lambda (u: T).(\lambda (H3: (eq T (THead (Flat Cast) u t0) (THead
 u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: 
 T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1 (lift (S O) O t2))) H4)))))))) y x 
 H0))) H)))).
+(* COMMENTS
+Initial nodes: 3436
+END *)
 
 theorem pr0_gen_lift:
  \forall (t1: T).(\forall (x: T).(\forall (h: nat).(\forall (d: nat).((pr0 
@@ -1991,4 +2012,7 @@ T).(eq T (lift h x1 x4) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Flat
 Cast) x2 x3) t4)) x4 (refl_equal T (lift h x1 x4)) (pr0_tau x3 x4 H7 x2)) t3 
 H_x)))) (H2 x3 x1 H6)) x0 H4)))))) (lift_gen_flat Cast u t2 x0 h x1 
 H3)))))))))) y x H0))))) H))))).
+(* COMMENTS
+Initial nodes: 7569
+END *)