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

diff --git a/matita/matita/contribs/lambdadelta/basic_1/pc1/props.ma b/matita/matita/contribs/lambdadelta/basic_1/pc1/props.ma
index faaa213cd..86e794a79 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/pc1/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/pc1/props.ma
@@ -18,27 +18,27 @@ include "basic_1/pc1/defs.ma".
 
 include "basic_1/pr1/pr1.ma".
 
-theorem pc1_pr0_r:
+lemma pc1_pr0_r:
  \forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to (pc1 t1 t2)))
 \def
  \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr0 t1 t2)).(ex_intro2 T 
 (\lambda (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t2 t)) t2 (pr1_pr0 t1 t2 H) 
 (pr1_refl t2)))).
 
-theorem pc1_pr0_x:
+lemma pc1_pr0_x:
  \forall (t1: T).(\forall (t2: T).((pr0 t2 t1) \to (pc1 t1 t2)))
 \def
  \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr0 t2 t1)).(ex_intro2 T 
 (\lambda (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t2 t)) t1 (pr1_refl t1) 
 (pr1_pr0 t2 t1 H)))).
 
-theorem pc1_refl:
+lemma pc1_refl:
  \forall (t: T).(pc1 t t)
 \def
  \lambda (t: T).(ex_intro2 T (\lambda (t0: T).(pr1 t t0)) (\lambda (t0: 
 T).(pr1 t t0)) t (pr1_refl t) (pr1_refl t)).
 
-theorem pc1_pr0_u:
+lemma pc1_pr0_u:
  \forall (t2: T).(\forall (t1: T).((pr0 t1 t2) \to (\forall (t3: T).((pc1 t2 
 t3) \to (pc1 t1 t3)))))
 \def
@@ -49,7 +49,7 @@ T).(\lambda (H2: (pr1 t2 x)).(\lambda (H3: (pr1 t3 x)).(ex_intro2 T (\lambda
 (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t3 t)) x (pr1_sing t2 t1 H x H2) 
 H3)))) H1)))))).
 
-theorem pc1_s:
+lemma pc1_s:
  \forall (t2: T).(\forall (t1: T).((pc1 t1 t2) \to (pc1 t2 t1)))
 \def
  \lambda (t2: T).(\lambda (t1: T).(\lambda (H: (pc1 t1 t2)).(let H0 \def H in 
@@ -58,7 +58,7 @@ t1) (\lambda (x: T).(\lambda (H1: (pr1 t1 x)).(\lambda (H2: (pr1 t2
 x)).(ex_intro2 T (\lambda (t: T).(pr1 t2 t)) (\lambda (t: T).(pr1 t1 t)) x H2 
 H1)))) H0)))).
 
-theorem pc1_head_1:
+lemma pc1_head_1:
  \forall (u1: T).(\forall (u2: T).((pc1 u1 u2) \to (\forall (t: T).(\forall 
 (k: K).(pc1 (THead k u1 t) (THead k u2 t))))))
 \def
@@ -70,7 +70,7 @@ T).(\lambda (k: K).(let H0 \def H in (ex2_ind T (\lambda (t0: T).(pr1 u1 t0))
 t) t0)) (THead k x t) (pr1_head_1 u1 x H1 t k) (pr1_head_1 u2 x H2 t k))))) 
 H0)))))).
 
-theorem pc1_head_2:
+lemma pc1_head_2:
  \forall (t1: T).(\forall (t2: T).((pc1 t1 t2) \to (\forall (u: T).(\forall 
 (k: K).(pc1 (THead k u t1) (THead k u t2))))))
 \def
@@ -97,7 +97,7 @@ x1)).(ex_intro2 T (\lambda (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t3 t)) x1
 (pr1_t x0 t1 H5 x1 H7) (pr1_t x t3 H3 x1 H8))))) (pr1_confluence t2 x0 H6 x 
 H2))))) H4))))) H1)))))).
 
-theorem pc1_pr0_u2:
+lemma pc1_pr0_u2:
  \forall (t0: T).(\forall (t1: T).((pr0 t0 t1) \to (\forall (t2: T).((pc1 t0 
 t2) \to (pc1 t1 t2)))))
 \def