uri renaming and new nodes count

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/pr3.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/pr3.ma
index 41a31b1f003b2ce59ccf4f6c961736da23068978..8d184aa586604e8c2d0d853100107577c4edd182 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/pr3.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/pr3.ma
@@ -14,17 +14,17 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/csubt/ty3.ma".
+include "Basic-1/csubt/ty3.ma".
 
-include "LambdaDelta-1/ty3/subst1.ma".
+include "Basic-1/ty3/subst1.ma".
 
-include "LambdaDelta-1/ty3/fsubst0.ma".
+include "Basic-1/ty3/fsubst0.ma".
 
-include "LambdaDelta-1/pc3/pc1.ma".
+include "Basic-1/pc3/pc1.ma".
 
-include "LambdaDelta-1/pc3/wcpr0.ma".
+include "Basic-1/pc3/wcpr0.ma".
 
-include "LambdaDelta-1/pc1/props.ma".
+include "Basic-1/pc1/props.ma".
 
 theorem ty3_sred_wcpr0_pr0:
  \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t: T).((ty3 g c1 
@@ -657,6 +657,9 @@ Cast) t0 t3) t3 (pr0_tau t3 t3 (pr0_refl t3) t0)))))) (ty3_correct g c2 t3 t0
 (H3 c2 H4 t3 (pr0_refl t3))))) t6 (sym_eq T t6 t4 H12))) t5 (sym_eq T t5 t2 
 H11))) u (sym_eq T u t3 H10))) H9)) H8 H6)))]) in (H6 (refl_equal T (THead 
 (Flat Cast) t3 t2)) (refl_equal T t4))))))))))))))) c1 t1 t H))))).
+(* COMMENTS
+Initial nodes: 14710
+END *)
 
 theorem ty3_sred_pr0:
  \forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to (\forall (g: G).(\forall 
@@ -665,6 +668,9 @@ theorem ty3_sred_pr0:
  \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr0 t1 t2)).(\lambda (g: 
 G).(\lambda (c: C).(\lambda (t: T).(\lambda (H0: (ty3 g c t1 
 t)).(ty3_sred_wcpr0_pr0 g c t1 t H0 c (wcpr0_refl c) t2 H))))))).
+(* COMMENTS
+Initial nodes: 47
+END *)
 
 theorem ty3_sred_pr1:
  \forall (t1: T).(\forall (t2: T).((pr1 t1 t2) \to (\forall (g: G).(\forall 
@@ -679,6 +685,9 @@ T).(\lambda (_: (pr1 t3 t5)).(\lambda (H2: ((\forall (g: G).(\forall (c:
 C).(\forall (t: T).((ty3 g c t3 t) \to (ty3 g c t5 t))))))).(\lambda (g: 
 G).(\lambda (c: C).(\lambda (t: T).(\lambda (H3: (ty3 g c t4 t)).(H2 g c t 
 (ty3_sred_pr0 t4 t3 H0 g c t H3)))))))))))) t1 t2 H))).
+(* COMMENTS
+Initial nodes: 151
+END *)
 
 theorem ty3_sred_pr2:
  \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr2 c t1 t2) \to (\forall 
@@ -696,6 +705,9 @@ t4)).(\lambda (t: T).(\lambda (H2: (subst0 i u t4 t)).(\lambda (g:
 G).(\lambda (t0: T).(\lambda (H3: (ty3 g c0 t3 t0)).(ty3_subst0 g c0 t4 t0 
 (ty3_sred_wcpr0_pr0 g c0 t3 t0 H3 c0 (wcpr0_refl c0) t4 H1) d u i H0 t 
 H2)))))))))))))) c t1 t2 H)))).
+(* COMMENTS
+Initial nodes: 205
+END *)
 
 theorem ty3_sred_pr3:
  \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr3 c t1 t2) \to (\forall 
@@ -710,4 +722,7 @@ T).(\lambda (t4: T).(\lambda (H0: (pr2 c t4 t3)).(\lambda (t5: T).(\lambda
 t3 t) \to (ty3 g c t5 t)))))).(\lambda (g: G).(\lambda (t: T).(\lambda (H3: 
 (ty3 g c t4 t)).(H2 g t (ty3_sred_pr2 c t4 t3 H0 g t H3))))))))))) t1 t2 
 H)))).
+(* COMMENTS
+Initial nodes: 151
+END *)