uri renaming and new nodes count

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Basic-1 / ty3 / fwd_nf2.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/fwd_nf2.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/fwd_nf2.ma
index 52e6c661f4b2b661a4053385f8e6e7c1e5bd5675..ca4e40c7bbf2a25dd4814949042fcc8eb2f90eb8 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/fwd_nf2.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/fwd_nf2.ma
@@ -14,11 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/ty3/arity_props.ma".
+include "Basic-1/ty3/arity_props.ma".
 
-include "LambdaDelta-1/pc3/nf2.ma".
+include "Basic-1/pc3/nf2.ma".
 
-include "LambdaDelta-1/nf2/fwd.ma".
+include "Basic-1/nf2/fwd.ma".
 
 theorem ty3_gen_appl_nf2:
  \forall (g: G).(\forall (c: C).(\forall (w: T).(\forall (v: T).(\forall (x: 
@@ -85,6 +85,9 @@ Abst) x0 x1) H1 (pc3_pr3_r c (THead (Bind Abst) x0 x1) (THead (Bind Abst) x5
 x6) H16)) (ty3_conv g c x5 x3 (ty3_sred_pr3 c x0 x5 H13 g x3 H6) w x0 H2 
 (pc3_pr3_r c x0 x5 H13)) H15)))))))) H11))))) H8)))))) H5))))) H3)))))))) 
 (ty3_gen_appl g c w v x H))))))).
+(* COMMENTS
+Initial nodes: 1289
+END *)
 
 theorem ty3_inv_lref_nf2_pc3:
  \forall (g: G).(\forall (c: C).(\forall (u1: T).(\forall (i: nat).((ty3 g c 
@@ -196,6 +199,9 @@ t1) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort
 _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) 
 \Rightarrow True])) I (TLRef i) H5) in (False_ind (ex T (\lambda (u: T).(eq T 
 u2 (lift (S i) O u)))) H9))))))))))))))) c y u1 H0))) H))))).
+(* COMMENTS
+Initial nodes: 2175
+END *)
 
 theorem ty3_inv_lref_nf2:
  \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (i: nat).((ty3 g c 
@@ -205,6 +211,9 @@ T).(eq T u (lift (S i) O u0))))))))))
  \lambda (g: G).(\lambda (c: C).(\lambda (u: T).(\lambda (i: nat).(\lambda 
 (H: (ty3 g c (TLRef i) u)).(\lambda (H0: (nf2 c (TLRef i))).(\lambda (H1: 
 (nf2 c u)).(ty3_inv_lref_nf2_pc3 g c u i H H0 u H1 (pc3_refl c u)))))))).
+(* COMMENTS
+Initial nodes: 57
+END *)
 
 theorem ty3_inv_appls_lref_nf2:
  \forall (g: G).(\forall (c: C).(\forall (vs: TList).(\forall (u1: 
@@ -263,6 +272,9 @@ i) O u))) u1)) x H12 (pc3_t (THead (Flat Appl) t (THead (Bind Abst) x0 x1)) c
 (THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O x))) (pc3_thin_dx c 
 (THeads (Flat Appl) t0 (lift (S i) O x)) (THead (Bind Abst) x0 x1) H13 t 
 Appl) u1 H4))))) H11))))) H8)))))))) H3))))))))))) vs))).
+(* COMMENTS
+Initial nodes: 1213
+END *)
 
 theorem ty3_inv_lref_lref_nf2:
  \forall (g: G).(\forall (c: C).(\forall (i: nat).(\forall (j: nat).((ty3 g c 
@@ -283,4 +295,7 @@ j O)).(\lambda (_: (eq T x (TLRef j))).(lt_x_O j H6 (lt i j)))) H5)) (\lambda
 i) j) (eq T x (TLRef (minus j (S i)))) (lt i j) (\lambda (H6: (le (S i) 
 j)).(\lambda (_: (eq T x (TLRef (minus j (S i))))).H6)) H5)) H4))))) 
 H2))))))))).
+(* COMMENTS
+Initial nodes: 337
+END *)