X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fnf2%2Fiso.ma;h=39b8275804e983ddbd5e671a12a6eb9d29a1fb88;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=6a2ce00f8d303a62952ea4b8cba03af531b5a025;hpb=88a68a9c334646bc17314d5327cd3b790202acd6;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 6a2ce00f8..39b827580 100644
--- 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 *)