X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fwf3%2Fgetl.ma;h=8a8f13780c806ac02a1fdefd6ad45bfeb9c013cc;hb=8ae1653eb75d2b57c50e077c49cb9d078313ea9d;hp=08fd20cfd2a51a82390c726d5573acd20d021d0a;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/wf3/getl.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/wf3/getl.ma
index 08fd20cfd..8a8f13780 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/wf3/getl.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/wf3/getl.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/wf3/clear.ma".
+include "Basic-1/wf3/clear.ma".
 
-include "LambdaDelta-1/ty3/dec.ma".
+include "Basic-1/ty3/dec.ma".
 
 theorem wf3_getl_conf:
  \forall (b: B).(\forall (i: nat).(\forall (c1: C).(\forall (d1: C).(\forall 
@@ -138,6 +138,9 @@ C).(wf3 g d1 d2)) x (getl_head (Bind Void) n x0 (CHead x (Bind b) v) H12
 (CHead d1 (Bind b) v))).(let H_y \def (wf3_gen_flat1 g c c2 t f H4) in (H0 d1 
 v H5 g c2 H_y w H3))))) k H2 (getl_gen_S k c (CHead d1 (Bind b) v) t n 
 H1)))))))))))))) c1)))) i)).
+(* COMMENTS
+Initial nodes: 2531
+END *)
 
 theorem getl_wf3_trans:
  \forall (i: nat).(\forall (c1: C).(\forall (d1: C).((getl i c1 d1) \to 
@@ -196,4 +199,7 @@ n) c2 d2))) (\lambda (x: C).(\lambda (H5: (wf3 g c x)).(\lambda (H6: (getl (S
 n) x d2)).(ex_intro2 C (\lambda (c2: C).(wf3 g (CHead c (Flat f) t) c2)) 
 (\lambda (c2: C).(getl (S n) c2 d2)) x (wf3_flat g c x H5 t f) H6)))) H4))))) 
 k (getl_gen_S k c d1 t n H1))))))))))) c1)))) i).
+(* COMMENTS
+Initial nodes: 1139
+END *)