X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fwf3%2Fgetl.ma;h=9c5fc73f5d55a4b975e3d7139ccd1ae448e47956;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=c8a7aa3116546643316b7be34f6b3ffb23a4da17;hpb=639e798161afea770f41d78673c0fe3be4125beb;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/wf3/getl.ma b/matita/matita/contribs/lambdadelta/basic_1/wf3/getl.ma
index c8a7aa311..9c5fc73f5 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/wf3/getl.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/wf3/getl.ma
@@ -18,7 +18,7 @@ include "basic_1/wf3/clear.ma".
 
 include "basic_1/ty3/dec.ma".
 
-theorem wf3_getl_conf:
+lemma wf3_getl_conf:
  \forall (b: B).(\forall (i: nat).(\forall (c1: C).(\forall (d1: C).(\forall 
 (v: T).((getl i c1 (CHead d1 (Bind b) v)) \to (\forall (g: G).(\forall (c2: 
 C).((wf3 g c1 c2) \to (\forall (w: T).((ty3 g d1 v w) \to (ex2 C (\lambda 
@@ -139,7 +139,7 @@ C).(wf3 g d1 d2)) x (getl_head (Bind Void) n x0 (CHead x (Bind b) v) H12
 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)).
 
-theorem getl_wf3_trans:
+lemma getl_wf3_trans:
  \forall (i: nat).(\forall (c1: C).(\forall (d1: C).((getl i c1 d1) \to 
 (\forall (g: G).(\forall (d2: C).((wf3 g d1 d2) \to (ex2 C (\lambda (c2: 
 C).(wf3 g c1 c2)) (\lambda (c2: C).(getl i c2 d2)))))))))