X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fpr2%2Fclen.ma;h=df9ea1fd97862a973cf92a6e8f585b29f148d838;hb=d6a9ed2a08fcc4e3e26a40cde8cab88c2c69cb3a;hp=ab6e6ef402e4dd497c77cb0388f5611244c4823a;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

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 ab6e6ef40..df9ea1fd9 100644
--- 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 *)