Procedural : tentative update to the new letin cic construction

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / LambdaDelta-1 / nf2 / props.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/props.ma
index 7dfefe20356238cdfff14a7cd0f3c406bf1ad6ad..17e87d94dbc87080e61fbd8ad9642b7d10ab38ee 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/props.ma
@@ -14,11 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/props".
+include "LambdaDelta-1/nf2/defs.ma".
 
-include "nf2/defs.ma".
-
-include "pr2/fwd.ma".
+include "LambdaDelta-1/pr2/fwd.ma".
 
 theorem nf2_sort:
  \forall (c: C).(\forall (n: nat).(nf2 c (TSort n)))
@@ -95,7 +93,7 @@ TList).((nfs2 c vs) \to (nf2 c (THeads (Flat Appl) vs (TLRef i)))))))
 (Flat Appl) t (TLRef i))))) (\lambda (_: True).H) (\lambda (t: T).(\lambda 
 (t0: TList).(\lambda (H0: (((nfs2 c t0) \to (nf2 c (THeads (Flat Appl) t0 
 (TLRef i)))))).(\lambda (H1: (land (nf2 c t) (nfs2 c t0))).(let H2 \def H1 in 
-(and_ind (nf2 c t) (nfs2 c t0) (nf2 c (THead (Flat Appl) t (THeads (Flat 
+(land_ind (nf2 c t) (nfs2 c t0) (nf2 c (THead (Flat Appl) t (THeads (Flat 
 Appl) t0 (TLRef i)))) (\lambda (H3: (nf2 c t)).(\lambda (H4: (nfs2 c 
 t0)).(let H_y \def (H0 H4) in (\lambda (t2: T).(\lambda (H5: (pr2 c (THead 
 (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t2)).(let H6 \def