(* 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)))
(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