flavour and source information exported for the objects of lambdadelta version 1

[helm.git] / matita / matita / contribs / lambdadelta / basic_1 / nf2 / iso.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_1/nf2/iso.ma b/matita/matita/contribs/lambdadelta/basic_1/nf2/iso.ma
index bd34df9dae7769abdeb14d8cc79896853c796182..39b8275804e983ddbd5e671a12a6eb9d29a1fb88 100644 (file)
--- 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))))))