uri renaming and new nodes count

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/dec.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/dec.ma
index 1936dd061854b1d4c1c655e62aeb3b10e70ccf82..c176d635e627ec621d1af035589828002222cfad 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/dec.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/dec.ma
@@ -14,11 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/pc3/dec.ma".
+include "Basic-1/pc3/dec.ma".
 
-include "LambdaDelta-1/getl/flt.ma".
+include "Basic-1/getl/flt.ma".
 
-include "LambdaDelta-1/getl/dec.ma".
+include "Basic-1/getl/dec.ma".
 
 theorem ty3_inference:
  \forall (g: G).(\forall (c: C).(\forall (t1: T).(or (ex T (\lambda (t2: 
@@ -432,4 +432,7 @@ t3)).(ex3_ind T (\lambda (t4: T).(pc3 c2 (THead (Flat Cast) t4 t) t3))
 T).(ty3 g c2 x0 t4)) False (\lambda (x: T).(\lambda (_: (ty3 g c2 x0 x)).(H5 
 x0 H9))) (ty3_correct g c2 t x0 H9)))))) (ty3_gen_cast g c2 t0 t t3 H6)))))) 
 H4))) f H2))) k H1))))))) t2))) c t1))).
+(* COMMENTS
+Initial nodes: 9001
+END *)