X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fgetl%2Fclear.ma;h=de0a85bd316e0beb06b1b5abb27334a103f9d38d;hb=de77f79d60ee3c1d30fe03469172950b557441f3;hp=a08c5da27f8df90350291429a6030ca21788adfb;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/getl/clear.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/getl/clear.ma
index a08c5da27..de0a85bd3 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/getl/clear.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/getl/clear.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/getl/props.ma".
+include "Basic-1/getl/props.ma".
 
-include "LambdaDelta-1/clear/drop.ma".
+include "Basic-1/clear/drop.ma".
 
 theorem clear_getl_trans:
  \forall (i: nat).(\forall (c2: C).(\forall (c3: C).((getl i c2 c3) \to 
@@ -47,6 +47,9 @@ c3)).(\lambda (c1: C).(\lambda (H2: (clear c1 (CHead c k t))).(K_ind (\lambda
 H6) H7)))) H5))))) (\lambda (f: F).(\lambda (_: (getl (S n) (CHead c (Flat f) 
 t) c3)).(\lambda (H4: (clear c1 (CHead c (Flat f) t))).(clear_gen_flat_r f c1 
 c t H4 (getl (S n) c1 c3))))) k H1 H2))))))))) c2)))) i).
+(* COMMENTS
+Initial nodes: 525
+END *)
 
 theorem getl_clear_trans:
  \forall (i: nat).(\forall (c1: C).(\forall (c2: C).((getl i c1 c2) \to 
@@ -65,6 +68,9 @@ in (let H7 \def (eq_ind C c2 (\lambda (c: C).(clear c c3)) H0 (CHead x1 (Bind
 x0) x2) H5) in (eq_ind_r C (CHead x1 (Bind x0) x2) (\lambda (c: C).(getl i c1 
 c)) (getl_intro i c1 (CHead x1 (Bind x0) x2) x H2 H6) c3 (clear_gen_bind x0 
 x1 c3 x2 H7)))))))) H4))))) H1))))))).
+(* COMMENTS
+Initial nodes: 269
+END *)
 
 theorem getl_clear_bind:
  \forall (b: B).(\forall (c: C).(\forall (e1: C).(\forall (v: T).((clear c 
@@ -103,6 +109,9 @@ n c0 e2 H8 t) b0 H6))))) H4)) H3)))) (\lambda (f: F).(\lambda (H2: (clear
 (CHead c0 (Flat f) t) (CHead e1 (Bind b) v))).(getl_flat c0 e2 (S n) (H e1 v 
 (clear_gen_flat f c0 (CHead e1 (Bind b) v) t H2) e2 n H1) f t))) k 
 H0))))))))))) c)).
+(* COMMENTS
+Initial nodes: 599
+END *)
 
 theorem getl_clear_conf:
  \forall (i: nat).(\forall (c1: C).(\forall (c3: C).((getl i c1 c3) \to 
@@ -138,4 +147,7 @@ t) c3)).(\lambda (H4: (clear (CHead c (Bind b) t) c2)).(eq_ind_r C (CHead c
 (\lambda (f: F).(\lambda (H3: (getl (S n) (CHead c (Flat f) t) c3)).(\lambda 
 (H4: (clear (CHead c (Flat f) t) c2)).(H0 c3 (getl_gen_S (Flat f) c c3 t n 
 H3) c2 (clear_gen_flat f c c2 t H4))))) k H1 H2))))))))) c1)))) i).
+(* COMMENTS
+Initial nodes: 641
+END *)