update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_1 / arity / aprem.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_1/arity/aprem.ma b/matita/matita/contribs/lambdadelta/basic_1/arity/aprem.ma
index f91be4fff8021339dc43444349cdf438d1f52dca..4426607390107ce0b78a5865f0104415fe6d592d 100644 (file)
--- 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))))