till some patches

[helm.git] / matita / contribs / LAMBDA-TYPES / Level-1 / LambdaDelta / nf2 / iso.ma

diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/nf2/iso.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/nf2/iso.ma
index 61c56a0bef2cedf4d203c27cbace2c2a785db914..83eee6eb24148aefe08035355e770f2556a95ae2 100644 (file)
--- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/nf2/iso.ma
+++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/nf2/iso.ma
@@ -20,7 +20,7 @@ include "nf2/pr3.ma".
 
 include "pr3/fwd.ma".
 
-include "iso/fwd.ma".
+include "iso/props.ma".
 
 theorem nf2_iso_appls_lref:
  \forall (c: C).(\forall (i: nat).((nf2 c (TLRef i)) \to (\forall (vs: