X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fcsubt%2Fpc3.ma;h=60a4452e3d9756d6590efeb42254263bf51c6a55;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=900ba49e962521cffb9af6801a4749b7a37e4494;hpb=88a68a9c334646bc17314d5327cd3b790202acd6;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/csubt/pc3.ma b/matita/matita/contribs/lambdadelta/basic_1/csubt/pc3.ma
index 900ba49e9..60a4452e3 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/csubt/pc3.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/csubt/pc3.ma
@@ -14,11 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/csubt/getl.ma".
+include "basic_1/csubt/getl.ma".
 
-include "Basic-1/pc3/left.ma".
+include "basic_1/pc3/left.ma".
 
-theorem csubt_pr2:
+lemma csubt_pr2:
  \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((pr2 c1 
 t1 t2) \to (\forall (c2: C).((csubt g c1 c2) \to (pr2 c2 t1 t2)))))))
 \def
@@ -35,11 +35,8 @@ c2 H3) in (ex2_ind C (\lambda (d2: C).(csubt g d d2)) (\lambda (d2: C).(getl
 i c2 (CHead d2 (Bind Abbr) u))) (pr2 c2 t3 t) (\lambda (x: C).(\lambda (_: 
 (csubt g d x)).(\lambda (H6: (getl i c2 (CHead x (Bind Abbr) u))).(pr2_delta 
 c2 x u i H6 t3 t4 H1 t H2)))) H4)))))))))))))) c1 t1 t2 H))))).
-(* COMMENTS
-Initial nodes: 245
-END *)
 
-theorem csubt_pc3:
+lemma csubt_pc3:
  \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((pc3 c1 
 t1 t2) \to (\forall (c2: C).((csubt g c1 c2) \to (pc3 c2 t1 t2)))))))
 \def
@@ -56,7 +53,4 @@ t0 t3)).(\lambda (t4: T).(\lambda (_: (pc3 c1 t0 t4)).(\lambda (H2: ((\forall
 (c2: C).((csubt g c1 c2) \to (pc3 c2 t0 t4))))).(\lambda (c2: C).(\lambda 
 (H3: (csubt g c1 c2)).(pc3_t t0 c2 t3 (pc3_pr2_x c2 t3 t0 (csubt_pr2 g c1 t0 
 t3 H0 c2 H3)) t4 (H2 c2 H3)))))))))) t1 t2 H))))).
-(* COMMENTS
-Initial nodes: 245
-END *)