uri renaming and new nodes count

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Basic-1 / sty0 / fwd.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/sty0/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/sty0/fwd.ma
index 873abbc80e00069208d3171a8e6ab3eb11bfbdef..134ec3c107c627ab935d27abbb28df6fd8076574 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/sty0/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/sty0/fwd.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/sty0/defs.ma".
+include "Basic-1/sty0/defs.ma".
 
 theorem sty0_gen_sort:
  \forall (g: G).(\forall (c: C).(\forall (x: T).(\forall (n: nat).((sty0 g c 
@@ -70,6 +70,9 @@ return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
 \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n) H5) in 
 (False_ind (eq T (THead (Flat Cast) v2 t2) (TSort (next g n))) H6)))))))))))) 
 c y x H0))) H))))).
+(* COMMENTS
+Initial nodes: 869
+END *)
 
 theorem sty0_gen_lref:
  \forall (g: G).(\forall (c: C).(\forall (x: T).(\forall (n: nat).((sty0 g c 
@@ -244,6 +247,9 @@ T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u))))) (\lambda (e:
 C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda 
 (u: T).(\lambda (_: T).(eq T (THead (Flat Cast) v2 t2) (lift (S n) O u))))))) 
 H6)))))))))))) c y x H0))) H))))).
+(* COMMENTS
+Initial nodes: 3231
+END *)
 
 theorem sty0_gen_bind:
  \forall (g: G).(\forall (b: B).(\forall (c: C).(\forall (u: T).(\forall (t1: 
@@ -348,6 +354,9 @@ u) t1 t3)) (\lambda (t3: T).(eq T t2 (THead (Bind b) u t3))))))).(\lambda
 True])])) I (THead (Bind b) u t1) H5) in (False_ind (ex2 T (\lambda (t3: 
 T).(sty0 g (CHead c0 (Bind b) u) t1 t3)) (\lambda (t3: T).(eq T (THead (Flat 
 Cast) v2 t2) (THead (Bind b) u t3)))) H6)))))))))))) c y x H0))) H))))))).
+(* COMMENTS
+Initial nodes: 1975
+END *)
 
 theorem sty0_gen_appl:
  \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t1: T).(\forall (x: 
@@ -434,6 +443,9 @@ v2 (THead (Flat Appl) u t2))))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda
 H5) in (False_ind (ex2 T (\lambda (t3: T).(sty0 g c0 t1 t3)) (\lambda (t3: 
 T).(eq T (THead (Flat Cast) v2 t2) (THead (Flat Appl) u t3)))) H6)))))))))))) 
 c y x H0))) H)))))).
+(* COMMENTS
+Initial nodes: 1489
+END *)
 
 theorem sty0_gen_cast:
  \forall (g: G).(\forall (c: C).(\forall (v1: T).(\forall (t1: T).(\forall 
@@ -544,4 +556,7 @@ H8) in (ex3_2_intro T T (\lambda (v3: T).(\lambda (_: T).(sty0 g c0 v1 v3)))
 T).(\lambda (t3: T).(eq T (THead (Flat Cast) v2 t2) (THead (Flat Cast) v3 
 t3)))) v2 t2 H12 H10 (refl_equal T (THead (Flat Cast) v2 t2))))))))) 
 H6)))))))))))) c y x H0))) H)))))).
+(* COMMENTS
+Initial nodes: 1855
+END *)