X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fcsuba%2Farity.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fcsuba%2Farity.ma;h=7b35a4381bb36b2440172e20b3e2a68ca3c96b78;hb=8de8cf8adfa6fcda91047eb2c25535893ede046a;hp=3edfe33a3d7f28702c6b8b34fa851b022b7caad6;hpb=d2caaf419cb6c92cb5ca8615f8eac4e12f3ab728;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/csuba/arity.ma b/matita/matita/contribs/lambdadelta/basic_1/csuba/arity.ma
index 3edfe33a3..7b35a4381 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/csuba/arity.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/csuba/arity.ma
@@ -22,7 +22,7 @@ include "basic_1/arity/fwd.ma".
 
 include "basic_1/csubv/getl.ma".
 
-theorem csuba_arity:
+lemma csuba_arity:
  \forall (g: G).(\forall (c1: C).(\forall (t: T).(\forall (a: A).((arity g c1 
 t a) \to (\forall (c2: C).((csuba g c1 c2) \to (arity g c2 t a)))))))
 \def
@@ -101,7 +101,7 @@ g c2 t0 a1))))).(\lambda (a2: A).(\lambda (H2: (leq g a1 a2)).(\lambda (c2:
 C).(\lambda (H3: (csuba g c c2)).(arity_repl g c2 t0 a1 (H1 c2 H3) a2 
 H2)))))))))) c1 t a H))))).
 
-theorem csuba_arity_rev:
+lemma csuba_arity_rev:
  \forall (g: G).(\forall (c1: C).(\forall (t: T).(\forall (a: A).((arity g c1 
 t a) \to (\forall (c2: C).((csuba g c2 c1) \to ((csubv c2 c1) \to (arity g c2 
 t a))))))))