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

diff --git a/matita/matita/contribs/lambdadelta/basic_1/arity/aprem.ma b/matita/matita/contribs/lambdadelta/basic_1/arity/aprem.ma
index f91be4fff..442660739 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/arity/aprem.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/arity/aprem.ma
@@ -20,7 +20,7 @@ include "basic_1/arity/cimp.ma".
 
 include "basic_1/aprem/props.ma".
 
-theorem arity_aprem:
+lemma arity_aprem:
  \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (a: A).((arity g c t 
 a) \to (\forall (i: nat).(\forall (b: A).((aprem i a b) \to (ex2_3 C T nat 
 (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O d c))))