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

diff --git a/matita/matita/contribs/lambdadelta/basic_1/ty3/arity.ma b/matita/matita/contribs/lambdadelta/basic_1/ty3/arity.ma
index c90321ff4..438021239 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/ty3/arity.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/ty3/arity.ma
@@ -20,7 +20,7 @@ include "basic_1/arity/pr3.ma".
 
 include "basic_1/asucc/fwd.ma".
 
-theorem ty3_arity:
+lemma ty3_arity:
  \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t2: T).((ty3 g c 
 t1 t2) \to (ex2 A (\lambda (a1: A).(arity g c t1 a1)) (\lambda (a1: A).(arity 
 g c t2 (asucc g a1))))))))