X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fcsubv%2Fclear.ma;h=4f4a012727acf4b2a72e238463f3335565fbfba2;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=80cfb2fa86f84286dce8a1ebcd6fbee9540a04bb;hpb=3cfed03c2025e778a5e62d9549b674dbfc6453bd;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/csubv/clear.ma b/matita/matita/contribs/lambdadelta/basic_1/csubv/clear.ma
index 80cfb2fa8..4f4a01272 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/csubv/clear.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/csubv/clear.ma
@@ -18,7 +18,7 @@ include "basic_1/csubv/fwd.ma".
 
 include "basic_1/clear/fwd.ma".
 
-theorem csubv_clear_conf:
+lemma csubv_clear_conf:
  \forall (c1: C).(\forall (c2: C).((csubv c1 c2) \to (\forall (b1: 
 B).(\forall (d1: C).(\forall (v1: T).((clear c1 (CHead d1 (Bind b1) v1)) \to 
 (ex2_3 B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv d1 
@@ -105,7 +105,7 @@ B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv d1 d2))))
 v2) (CHead d2 (Bind b2) v3))))) x0 x1 x2 H4 (clear_flat c4 (CHead x1 (Bind 
 x0) x2) H5 f2 v2))))))) H3))))))))))))))) c1 c2 H))).
 
-theorem csubv_clear_conf_void:
+lemma csubv_clear_conf_void:
  \forall (c1: C).(\forall (c2: C).((csubv c1 c2) \to (\forall (d1: 
 C).(\forall (v1: T).((clear c1 (CHead d1 (Bind Void) v1)) \to (ex2_2 C T 
 (\lambda (d2: C).(\lambda (_: T).(csubv d1 d2))) (\lambda (d2: C).(\lambda