uri renaming and new nodes count

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Basic-1 / pr2 / clen.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr2/clen.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr2/clen.ma
index ab6e6ef402e4dd497c77cb0388f5611244c4823a..df9ea1fd97862a973cf92a6e8f585b29f148d838 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr2/clen.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr2/clen.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/pr2/props.ma".
+include "Basic-1/pr2/props.ma".
 
-include "LambdaDelta-1/clen/getl.ma".
+include "Basic-1/clen/getl.ma".
 
 theorem pr2_gen_ctail:
  \forall (k: K).(\forall (c: C).(\forall (u: T).(\forall (t1: T).(\forall 
@@ -75,6 +75,9 @@ t))) (ex3_intro T (\lambda (_: T).(eq K (Bind Abbr) (Bind Abbr))) (\lambda
 (t0: T).(pr0 t3 t0)) (\lambda (t0: T).(subst0 (clen c) u t0 t)) t4 
 (refl_equal K (Bind Abbr)) H2 H13)) k H9)))))))) H7)) H6))))))))))))))) y t1 
 t2 H0))) H)))))).
+(* COMMENTS
+Initial nodes: 1161
+END *)
 
 theorem pr2_gen_cbind:
  \forall (b: B).(\forall (c: C).(\forall (v: T).(\forall (t1: T).(\forall 
@@ -129,6 +132,9 @@ nat nat (\lambda (e: nat).e) i (S x) H8) in (let H11 \def (eq_ind nat i
 (Bind b) (pr2_delta (CHead c (Bind b) v) d u (S x) (getl_clear_bind b (CHead 
 c (Bind b) v) c v (clear_bind b c v) (CHead d (Bind Abbr) u) x H9) t3 t4 H2 t 
 H11))))))) H7)) H6))))))))))))))) y t1 t2 H0))) H)))))).
+(* COMMENTS
+Initial nodes: 1085
+END *)
 
 theorem pr2_gen_cflat:
  \forall (f: F).(\forall (c: C).(\forall (v: T).(\forall (t1: T).(\forall 
@@ -149,4 +155,7 @@ T).(\lambda (t4: T).(\lambda (H2: (pr0 t3 t4)).(\lambda (t: T).(\lambda (H3:
 c (Flat f) v) H4) in (let H_y \def (getl_gen_flat f c (CHead d (Bind Abbr) u) 
 v i H5) in (pr2_delta c d u i H_y t3 t4 H2 t H3)))))))))))))) y t1 t2 H0))) 
 H)))))).
+(* COMMENTS
+Initial nodes: 293
+END *)