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

diff --git a/matita/matita/contribs/lambdadelta/basic_1/pr0/props.ma b/matita/matita/contribs/lambdadelta/basic_1/pr0/props.ma
index c3558ca72..d1c31fcc7 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/pr0/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/pr0/props.ma
@@ -18,7 +18,7 @@ include "basic_1/pr0/fwd.ma".
 
 include "basic_1/subst0/props.ma".
 
-theorem pr0_lift:
+lemma pr0_lift:
  \forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to (\forall (h: nat).(\forall 
 (d: nat).(pr0 (lift h d t1) (lift h d t2))))))
 \def
@@ -128,7 +128,7 @@ d u) (lift h (s (Flat Cast) d) t3)) (\lambda (t: T).(pr0 t (lift h d t4)))
 (lift h d (THead (Flat Cast) u t3)) (lift_head (Flat Cast) u t3 h d))))))))) 
 t1 t2 H))).
 
-theorem pr0_gen_abbr:
+lemma pr0_gen_abbr:
  \forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr0 (THead (Bind Abbr) u1 
 t1) x) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T x (THead 
 (Bind Abbr) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda 
@@ -358,7 +358,7 @@ T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0))
 (\lambda (y0: T).(subst0 O u2 y0 t3))))))) (pr0 t1 (lift (S O) O t2))) 
 H4)))))))) y x H0))) H)))).
 
-theorem pr0_gen_void:
+lemma pr0_gen_void:
  \forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr0 (THead (Bind Void) u1 
 t1) x) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T x (THead 
 (Bind Void) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda