X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fwf3%2Fty3.ma;h=e47d4a2e0d1032ae1060f4939ae71eb30bf92efb;hb=d3548c16f481b14ce94e64c790bc767c59590050;hp=1a348324b29d9dacc66413719d52de721148c357;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/wf3/ty3.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/wf3/ty3.ma
index 1a348324b..e47d4a2e0 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/wf3/ty3.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/wf3/ty3.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/wf3/getl.ma".
+include "Basic-1/wf3/getl.ma".
 
 theorem wf3_pr2_conf:
  \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((pr2 c1 
@@ -40,6 +40,9 @@ g c2 H3 x H6) in (let H7 \def H_x0 in (ex2_ind C (\lambda (d2: C).(getl i c2
 (\lambda (x0: C).(\lambda (H8: (getl i c2 (CHead x0 (Bind Abbr) u))).(\lambda 
 (_: (wf3 g d x0)).(pr2_delta c2 x0 u i H8 t3 t4 H1 t H2)))) H7))))) 
 H5)))))))))))))))))) c1 t1 t2 H))))).
+(* COMMENTS
+Initial nodes: 373
+END *)
 
 theorem wf3_pr3_conf:
  \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((pr3 c1 
@@ -57,6 +60,9 @@ c2) \to (\forall (u: T).((ty3 g c1 t3 u) \to (pr3 c2 t3 t5))))))).(\lambda
 (c2: C).(\lambda (H3: (wf3 g c1 c2)).(\lambda (u: T).(\lambda (H4: (ty3 g c1 
 t4 u)).(pr3_sing c2 t3 t4 (wf3_pr2_conf g c1 t4 t3 H0 c2 H3 u H4) t5 (H2 c2 
 H3 u (ty3_sred_pr2 c1 t4 t3 H0 g u H4))))))))))))) t1 t2 H))))).
+(* COMMENTS
+Initial nodes: 217
+END *)
 
 theorem wf3_pc3_conf:
  \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((pc3 c1 
@@ -71,6 +77,9 @@ c1 t2 u2)).(let H3 \def H in (ex2_ind T (\lambda (t: T).(pr3 c1 t1 t))
 (pr3 c1 t1 x)).(\lambda (H5: (pr3 c1 t2 x)).(pc3_pr3_t c2 t1 x (wf3_pr3_conf 
 g c1 t1 x H4 c2 H0 u1 H1) t2 (wf3_pr3_conf g c1 t2 x H5 c2 H0 u2 H2))))) 
 H3)))))))))))).
+(* COMMENTS
+Initial nodes: 153
+END *)
 
 theorem wf3_ty3_conf:
  \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((ty3 g c1 
@@ -123,4 +132,7 @@ C).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (ty3 g c t3 t4)).(\lambda
 T).(\lambda (_: (ty3 g c t4 t0)).(\lambda (H3: ((\forall (c2: C).((wf3 g c 
 c2) \to (ty3 g c2 t4 t0))))).(\lambda (c2: C).(\lambda (H4: (wf3 g c 
 c2)).(ty3_cast g c2 t3 t4 (H1 c2 H4) t0 (H3 c2 H4)))))))))))) c1 t1 t2 H))))).
+(* COMMENTS
+Initial nodes: 1027
+END *)