X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fnf2%2Fiso.ma;h=39b8275804e983ddbd5e671a12a6eb9d29a1fb88;hb=8f5533bd34e93eee2a14cdcfd0595be65651bfa7;hp=bd34df9dae7769abdeb14d8cc79896853c796182;hpb=639e798161afea770f41d78673c0fe3be4125beb;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/nf2/iso.ma b/matita/matita/contribs/lambdadelta/basic_1/nf2/iso.ma
index bd34df9da..39b827580 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/nf2/iso.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/nf2/iso.ma
@@ -18,7 +18,7 @@ include "basic_1/nf2/pr3.ma".
 
 include "basic_1/iso/props.ma".
 
-theorem nf2_iso_appls_lref:
+lemma nf2_iso_appls_lref:
  \forall (c: C).(\forall (i: nat).((nf2 c (TLRef i)) \to (\forall (vs: 
 TList).(\forall (u: T).((pr3 c (THeads (Flat Appl) vs (TLRef i)) u) \to (iso 
 (THeads (Flat Appl) vs (TLRef i)) u))))))