Procedural : tentative update to the new letin cic construction

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/arity.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/arity.ma
index 0b17ee3784a311098a09ea7c46aa9d626092b70f..9fe69d76692f9cbd23b064319cd6d8d835814ef3 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/arity.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/arity.ma
@@ -176,7 +176,7 @@ nat (\lambda (ws: TList).(\lambda (i: nat).(eq T t0 (THeads (Flat Appl) ws
 (TLRef i))))) (\lambda (ws: TList).(\lambda (_: nat).(nfs2 (CHead c0 (Bind 
 Abst) u) ws))) (\lambda (_: TList).(\lambda (i: nat).(nf2 (CHead c0 (Bind 
 Abst) u) (TLRef i))))))))).(\lambda (H4: (nf2 c0 (THead (Bind Abst) u 
-t0))).(let H5 \def (nf2_gen_abst c0 u t0 H4) in (and_ind (nf2 c0 u) (nf2 
+t0))).(let H5 \def (nf2_gen_abst c0 u t0 H4) in (land_ind (nf2 c0 u) (nf2 
 (CHead c0 (Bind Abst) u) t0) (or3 (ex3_2 T T (\lambda (w: T).(\lambda (u0: 
 T).(eq T (THead (Bind Abst) u t0) (THead (Bind Abst) w u0)))) (\lambda (w: 
 T).(\lambda (_: T).(nf2 c0 w))) (\lambda (w: T).(\lambda (u0: T).(nf2 (CHead 
@@ -213,21 +213,21 @@ t0 (TSort n)))) (ex3_2 TList nat (\lambda (ws: TList).(\lambda (i: nat).(eq T
 t0 (THeads (Flat Appl) ws (TLRef i))))) (\lambda (ws: TList).(\lambda (_: 
 nat).(nfs2 c0 ws))) (\lambda (_: TList).(\lambda (i: nat).(nf2 c0 (TLRef 
 i))))))))).(\lambda (H4: (nf2 c0 (THead (Flat Appl) u t0))).(let H5 \def 
-(nf2_gen_flat Appl c0 u t0 H4) in (and_ind (nf2 c0 u) (nf2 c0 t0) (or3 (ex3_2 
-T T (\lambda (w: T).(\lambda (u0: T).(eq T (THead (Flat Appl) u t0) (THead 
-(Bind Abst) w u0)))) (\lambda (w: T).(\lambda (_: T).(nf2 c0 w))) (\lambda 
-(w: T).(\lambda (u0: T).(nf2 (CHead c0 (Bind Abst) w) u0)))) (ex nat (\lambda 
-(n: nat).(eq T (THead (Flat Appl) u t0) (TSort n)))) (ex3_2 TList nat 
-(\lambda (ws: TList).(\lambda (i: nat).(eq T (THead (Flat Appl) u t0) (THeads 
-(Flat Appl) ws (TLRef i))))) (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c0 
-ws))) (\lambda (_: TList).(\lambda (i: nat).(nf2 c0 (TLRef i)))))) (\lambda 
-(H6: (nf2 c0 u)).(\lambda (H7: (nf2 c0 t0)).(let H_x \def (H3 H7) in (let H8 
-\def H_x in (or3_ind (ex3_2 T T (\lambda (w: T).(\lambda (u0: T).(eq T t0 
+(nf2_gen_flat Appl c0 u t0 H4) in (land_ind (nf2 c0 u) (nf2 c0 t0) (or3 
+(ex3_2 T T (\lambda (w: T).(\lambda (u0: T).(eq T (THead (Flat Appl) u t0) 
 (THead (Bind Abst) w u0)))) (\lambda (w: T).(\lambda (_: T).(nf2 c0 w))) 
 (\lambda (w: T).(\lambda (u0: T).(nf2 (CHead c0 (Bind Abst) w) u0)))) (ex nat 
-(\lambda (n: nat).(eq T t0 (TSort n)))) (ex3_2 TList nat (\lambda (ws: 
-TList).(\lambda (i: nat).(eq T t0 (THeads (Flat Appl) ws (TLRef i))))) 
-(\lambda (ws: TList).(\lambda (_: nat).(nfs2 c0 ws))) (\lambda (_: 
+(\lambda (n: nat).(eq T (THead (Flat Appl) u t0) (TSort n)))) (ex3_2 TList 
+nat (\lambda (ws: TList).(\lambda (i: nat).(eq T (THead (Flat Appl) u t0) 
+(THeads (Flat Appl) ws (TLRef i))))) (\lambda (ws: TList).(\lambda (_: 
+nat).(nfs2 c0 ws))) (\lambda (_: TList).(\lambda (i: nat).(nf2 c0 (TLRef 
+i)))))) (\lambda (H6: (nf2 c0 u)).(\lambda (H7: (nf2 c0 t0)).(let H_x \def 
+(H3 H7) in (let H8 \def H_x in (or3_ind (ex3_2 T T (\lambda (w: T).(\lambda 
+(u0: T).(eq T t0 (THead (Bind Abst) w u0)))) (\lambda (w: T).(\lambda (_: 
+T).(nf2 c0 w))) (\lambda (w: T).(\lambda (u0: T).(nf2 (CHead c0 (Bind Abst) 
+w) u0)))) (ex nat (\lambda (n: nat).(eq T t0 (TSort n)))) (ex3_2 TList nat 
+(\lambda (ws: TList).(\lambda (i: nat).(eq T t0 (THeads (Flat Appl) ws (TLRef 
+i))))) (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c0 ws))) (\lambda (_: 
 TList).(\lambda (i: nat).(nf2 c0 (TLRef i))))) (or3 (ex3_2 T T (\lambda (w: 
 T).(\lambda (u0: T).(eq T (THead (Flat Appl) u t0) (THead (Bind Abst) w 
 u0)))) (\lambda (w: T).(\lambda (_: T).(nf2 c0 w))) (\lambda (w: T).(\lambda