X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fwf3%2Fty3.ma;h=2958902bda14ea3dbe6e078ade9ba8a4f6fca067;hb=c7b50fec51b9a25d5bc536f44e54179fd53efb44;hp=be4d21960d552ed59a1a6c72b5e2e50964632cae;hpb=639e798161afea770f41d78673c0fe3be4125beb;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/wf3/ty3.ma b/matita/matita/contribs/lambdadelta/basic_1/wf3/ty3.ma
index be4d21960..2958902bd 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/wf3/ty3.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/wf3/ty3.ma
@@ -16,7 +16,7 @@
 
 include "basic_1/wf3/getl.ma".
 
-theorem wf3_pr2_conf:
+lemma wf3_pr2_conf:
  \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((pr2 c1 
 t1 t2) \to (\forall (c2: C).((wf3 g c1 c2) \to (\forall (u: T).((ty3 g c1 t1 
 u) \to (pr2 c2 t1 t2)))))))))
@@ -41,7 +41,7 @@ g c2 H3 x H6) in (let H7 \def H_x0 in (ex2_ind C (\lambda (d2: C).(getl i c2
 (_: (wf3 g d x0)).(pr2_delta c2 x0 u i H8 t3 t4 H1 t H2)))) H7))))) 
 H5)))))))))))))))))) c1 t1 t2 H))))).
 
-theorem wf3_pr3_conf:
+lemma wf3_pr3_conf:
  \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((pr3 c1 
 t1 t2) \to (\forall (c2: C).((wf3 g c1 c2) \to (\forall (u: T).((ty3 g c1 t1 
 u) \to (pr3 c2 t1 t2)))))))))
@@ -58,7 +58,7 @@ c2) \to (\forall (u: T).((ty3 g c1 t3 u) \to (pr3 c2 t3 t5))))))).(\lambda
 t4 u)).(pr3_sing c2 t3 t4 (wf3_pr2_conf g c1 t4 t3 H0 c2 H3 u H4) t5 (H2 c2 
 H3 u (ty3_sred_pr2 c1 t4 t3 H0 g u H4))))))))))))) t1 t2 H))))).
 
-theorem wf3_pc3_conf:
+lemma wf3_pc3_conf:
  \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((pc3 c1 
 t1 t2) \to (\forall (c2: C).((wf3 g c1 c2) \to (\forall (u1: T).((ty3 g c1 t1 
 u1) \to (\forall (u2: T).((ty3 g c1 t2 u2) \to (pc3 c2 t1 t2)))))))))))
@@ -72,7 +72,7 @@ c1 t2 u2)).(let H3 \def H in (ex2_ind T (\lambda (t: T).(pr3 c1 t1 t))
 g c1 t1 x H4 c2 H0 u1 H1) t2 (wf3_pr3_conf g c1 t2 x H5 c2 H0 u2 H2))))) 
 H3)))))))))))).
 
-theorem wf3_ty3_conf:
+lemma wf3_ty3_conf:
  \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((ty3 g c1 
 t1 t2) \to (\forall (c2: C).((wf3 g c1 c2) \to (ty3 g c2 t1 t2)))))))
 \def