update in basic_2

[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 6a2ce00f8d303a62952ea4b8cba03af531b5a025..39b8275804e983ddbd5e671a12a6eb9d29a1fb88 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/nf2/iso.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/nf2/iso.ma
@@ -14,13 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/nf2/pr3.ma".
+include "basic_1/nf2/pr3.ma".
 
-include "Basic-1/pr3/fwd.ma".
+include "basic_1/iso/props.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))))))
@@ -124,7 +122,4 @@ x5)).(\lambda (_: (pr3 (CHead c (Bind x0) x5) x2 x3)).(let H_y \def (H0
 (THead (Bind x0) x1 x2) H5) in (iso_flats_lref_bind_false Appl x0 i x1 x2 t0 
 H_y (iso (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) 
 u))))))))))))))) H3)) H2))))))) vs)))).
-(* COMMENTS
-Initial nodes: 1817
-END *)