X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fty3%2Fnf2.ma;h=f76e4928957c5308bd1e97ddaaeaf5f314dfc61b;hb=de0eae04721942f08b7281664bfbc26badf5de84;hp=300238885d63e03f53e3ed9ceaf9c73d7e6520fc;hpb=5c1b44dfefa085fbb56e23047652d3650be9d855;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/nf2.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/nf2.ma
index 300238885..f76e49289 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/nf2.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/nf2.ma
@@ -14,13 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
+include "LambdaDelta-1/ty3/arity.ma".
 
+include "LambdaDelta-1/pc3/nf2.ma".
 
-include "ty3/arity.ma".
-
-include "pc3/nf2.ma".
-
-include "nf2/arity.ma".
+include "LambdaDelta-1/nf2/arity.ma".
 
 definition ty3_nf2_inv_abst_premise:
  C \to (T \to (T \to Prop))
@@ -102,26 +100,23 @@ x1)).(let H6 \def (eq_ind T t (\lambda (t0: T).(ty3 g c t0 (TSort m))) H
 (n: nat).(eq nat m (next g 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 c ws))) (\lambda (_: 
-TList).(\lambda (i: nat).(nf2 c (TLRef i))))))) (ex4_3_ind T T T (\lambda 
-(t2: T).(\lambda (_: T).(\lambda (_: T).(pc3 c (THead (Bind Abst) x0 t2) 
-(TSort m))))) (\lambda (_: T).(\lambda (t0: T).(\lambda (_: T).(ty3 g c x0 
-t0)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c (Bind 
-Abst) x0) x1 t2)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (t1: T).(ty3 g 
-(CHead c (Bind Abst) x0) t2 t1)))) (or (ex2 nat (\lambda (n: nat).(eq T 
-(THead (Bind Abst) x0 x1) (TSort n))) (\lambda (n: nat).(eq nat m (next g 
-n)))) (ex3_2 TList nat (\lambda (ws: TList).(\lambda (i: nat).(eq T (THead 
-(Bind Abst) x0 x1) (THeads (Flat Appl) ws (TLRef i))))) (\lambda (ws: 
+TList).(\lambda (i: nat).(nf2 c (TLRef i))))))) (ex3_2_ind T T (\lambda (t2: 
+T).(\lambda (_: T).(pc3 c (THead (Bind Abst) x0 t2) (TSort m)))) (\lambda (_: 
+T).(\lambda (t0: T).(ty3 g c x0 t0))) (\lambda (t2: T).(\lambda (_: T).(ty3 g 
+(CHead c (Bind Abst) x0) x1 t2))) (or (ex2 nat (\lambda (n: nat).(eq T (THead 
+(Bind Abst) x0 x1) (TSort n))) (\lambda (n: nat).(eq nat m (next g n)))) 
+(ex3_2 TList nat (\lambda (ws: TList).(\lambda (i: nat).(eq T (THead (Bind 
+Abst) x0 x1) (THeads (Flat Appl) ws (TLRef i))))) (\lambda (ws: 
 TList).(\lambda (_: nat).(nfs2 c ws))) (\lambda (_: TList).(\lambda (i: 
-nat).(nf2 c (TLRef i)))))) (\lambda (x2: T).(\lambda (x3: T).(\lambda (x4: 
-T).(\lambda (H7: (pc3 c (THead (Bind Abst) x0 x2) (TSort m))).(\lambda (_: 
-(ty3 g c x0 x3)).(\lambda (_: (ty3 g (CHead c (Bind Abst) x0) x1 
-x2)).(\lambda (_: (ty3 g (CHead c (Bind Abst) x0) x2 x4)).(pc3_gen_sort_abst 
+nat).(nf2 c (TLRef i)))))) (\lambda (x2: T).(\lambda (x3: T).(\lambda (H7: 
+(pc3 c (THead (Bind Abst) x0 x2) (TSort m))).(\lambda (_: (ty3 g c x0 
+x3)).(\lambda (_: (ty3 g (CHead c (Bind Abst) x0) x1 x2)).(pc3_gen_sort_abst 
 c x0 x2 m (pc3_s c (TSort m) (THead (Bind Abst) x0 x2) H7) (or (ex2 nat 
 (\lambda (n: nat).(eq T (THead (Bind Abst) x0 x1) (TSort n))) (\lambda (n: 
 nat).(eq nat m (next g n)))) (ex3_2 TList nat (\lambda (ws: TList).(\lambda 
 (i: nat).(eq T (THead (Bind Abst) x0 x1) (THeads (Flat Appl) ws (TLRef i))))) 
 (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c ws))) (\lambda (_: 
-TList).(\lambda (i: nat).(nf2 c (TLRef i)))))))))))))) (ty3_gen_bind g Abst c 
+TList).(\lambda (i: nat).(nf2 c (TLRef i)))))))))))) (ty3_gen_bind g Abst c 
 x0 x1 (TSort m) H6)) t H3))))))) H2)) (\lambda (H2: (ex nat (\lambda (n: 
 nat).(eq T t (TSort n))))).(ex_ind nat (\lambda (n: nat).(eq T t (TSort n))) 
 (or (ex2 nat (\lambda (n: nat).(eq T t (TSort n))) (\lambda (n: nat).(eq nat 
@@ -243,102 +238,97 @@ w u) t0)) (ex4_2 T T (\lambda (v: T).(\lambda (_: T).(eq T (THead (Bind Abst)
 x0 x1) (THead (Bind Abst) w v)))) (\lambda (_: T).(\lambda (w0: T).(ty3 g c w 
 w0))) (\lambda (v: T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) w) v u))) 
 (\lambda (v: T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) w) v)))) (\lambda 
-(x: T).(\lambda (H9: (ty3 g c (THead (Bind Abst) w u) x)).(ex4_3_ind T T T 
-(\lambda (t2: T).(\lambda (_: T).(\lambda (_: T).(pc3 c (THead (Bind Abst) w 
-t2) x)))) (\lambda (_: T).(\lambda (t0: T).(\lambda (_: T).(ty3 g c w t0)))) 
-(\lambda (t2: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) 
-w) u t2)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (t1: T).(ty3 g (CHead c 
-(Bind Abst) w) t2 t1)))) (ex4_2 T T (\lambda (v: T).(\lambda (_: T).(eq T 
-(THead (Bind Abst) x0 x1) (THead (Bind Abst) w v)))) (\lambda (_: T).(\lambda 
-(w0: T).(ty3 g c w w0))) (\lambda (v: T).(\lambda (_: T).(ty3 g (CHead c 
-(Bind Abst) w) v u))) (\lambda (v: T).(\lambda (_: T).(nf2 (CHead c (Bind 
-Abst) w) v)))) (\lambda (x2: T).(\lambda (x3: T).(\lambda (x4: T).(\lambda 
-(_: (pc3 c (THead (Bind Abst) w x2) x)).(\lambda (H11: (ty3 g c w 
-x3)).(\lambda (H12: (ty3 g (CHead c (Bind Abst) w) u x2)).(\lambda (_: (ty3 g 
-(CHead c (Bind Abst) w) x2 x4)).(ex4_3_ind T T T (\lambda (t2: T).(\lambda 
-(_: T).(\lambda (_: T).(pc3 c (THead (Bind Abst) x0 t2) (THead (Bind Abst) w 
-u))))) (\lambda (_: T).(\lambda (t0: T).(\lambda (_: T).(ty3 g c x0 t0)))) 
-(\lambda (t2: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) 
-x0) x1 t2)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (t1: T).(ty3 g (CHead 
-c (Bind Abst) x0) t2 t1)))) (ex4_2 T T (\lambda (v: T).(\lambda (_: T).(eq T 
-(THead (Bind Abst) x0 x1) (THead (Bind Abst) w v)))) (\lambda (_: T).(\lambda 
-(w0: T).(ty3 g c w w0))) (\lambda (v: T).(\lambda (_: T).(ty3 g (CHead c 
-(Bind Abst) w) v u))) (\lambda (v: T).(\lambda (_: T).(nf2 (CHead c (Bind 
-Abst) w) v)))) (\lambda (x5: T).(\lambda (x6: T).(\lambda (x7: T).(\lambda 
-(H14: (pc3 c (THead (Bind Abst) x0 x5) (THead (Bind Abst) w u))).(\lambda (_: 
-(ty3 g c x0 x6)).(\lambda (H16: (ty3 g (CHead c (Bind Abst) x0) x1 
-x5)).(\lambda (_: (ty3 g (CHead c (Bind Abst) x0) x5 x7)).(and_ind (pc3 c x0 
-w) (\forall (b: B).(\forall (u0: T).(pc3 (CHead c (Bind b) u0) x5 u))) (ex4_2 
-T T (\lambda (v: T).(\lambda (_: T).(eq T (THead (Bind Abst) x0 x1) (THead 
-(Bind Abst) w v)))) (\lambda (_: T).(\lambda (w0: T).(ty3 g c w w0))) 
+(x: T).(\lambda (H9: (ty3 g c (THead (Bind Abst) w u) x)).(ex3_2_ind T T 
+(\lambda (t2: T).(\lambda (_: T).(pc3 c (THead (Bind Abst) w t2) x))) 
+(\lambda (_: T).(\lambda (t0: T).(ty3 g c w t0))) (\lambda (t2: T).(\lambda 
+(_: T).(ty3 g (CHead c (Bind Abst) w) u t2))) (ex4_2 T T (\lambda (v: 
+T).(\lambda (_: T).(eq T (THead (Bind Abst) x0 x1) (THead (Bind Abst) w v)))) 
+(\lambda (_: T).(\lambda (w0: T).(ty3 g c w w0))) (\lambda (v: T).(\lambda 
+(_: T).(ty3 g (CHead c (Bind Abst) w) v u))) (\lambda (v: T).(\lambda (_: 
+T).(nf2 (CHead c (Bind Abst) w) v)))) (\lambda (x2: T).(\lambda (x3: 
+T).(\lambda (_: (pc3 c (THead (Bind Abst) w x2) x)).(\lambda (H11: (ty3 g c w 
+x3)).(\lambda (H12: (ty3 g (CHead c (Bind Abst) w) u x2)).(ex3_2_ind T T 
+(\lambda (t2: T).(\lambda (_: T).(pc3 c (THead (Bind Abst) x0 t2) (THead 
+(Bind Abst) w u)))) (\lambda (_: T).(\lambda (t0: T).(ty3 g c x0 t0))) 
+(\lambda (t2: T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) x0) x1 t2))) 
+(ex4_2 T T (\lambda (v: T).(\lambda (_: T).(eq T (THead (Bind Abst) x0 x1) 
+(THead (Bind Abst) w v)))) (\lambda (_: T).(\lambda (w0: T).(ty3 g c w w0))) 
 (\lambda (v: T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) w) v u))) 
 (\lambda (v: T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) w) v)))) (\lambda 
-(H18: (pc3 c x0 w)).(\lambda (H19: ((\forall (b: B).(\forall (u0: T).(pc3 
-(CHead c (Bind b) u0) x5 u))))).(let H_y \def (pc3_nf2 c x0 w H18 H6 H1) in 
-(let H20 \def (eq_ind T x0 (\lambda (t0: T).(ty3 g (CHead c (Bind Abst) t0) 
-x1 x5)) H16 w H_y) in (let H21 \def (eq_ind T x0 (\lambda (t0: T).(nf2 (CHead 
-c (Bind Abst) t0) x1)) H7 w H_y) in (eq_ind_r T w (\lambda (t0: T).(ex4_2 T T 
-(\lambda (v: T).(\lambda (_: T).(eq T (THead (Bind Abst) t0 x1) (THead (Bind 
-Abst) w v)))) (\lambda (_: T).(\lambda (w0: T).(ty3 g c w w0))) (\lambda (v: 
-T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) w) v u))) (\lambda (v: 
-T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) w) v))))) (ex4_2_intro T T 
-(\lambda (v: T).(\lambda (_: T).(eq T (THead (Bind Abst) w x1) (THead (Bind 
-Abst) w v)))) (\lambda (_: T).(\lambda (w0: T).(ty3 g c w w0))) (\lambda (v: 
+(x4: T).(\lambda (x5: T).(\lambda (H13: (pc3 c (THead (Bind Abst) x0 x4) 
+(THead (Bind Abst) w u))).(\lambda (_: (ty3 g c x0 x5)).(\lambda (H15: (ty3 g 
+(CHead c (Bind Abst) x0) x1 x4)).(and_ind (pc3 c x0 w) (\forall (b: 
+B).(\forall (u0: T).(pc3 (CHead c (Bind b) u0) x4 u))) (ex4_2 T T (\lambda 
+(v: T).(\lambda (_: T).(eq T (THead (Bind Abst) x0 x1) (THead (Bind Abst) w 
+v)))) (\lambda (_: T).(\lambda (w0: T).(ty3 g c w w0))) (\lambda (v: 
 T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) w) v u))) (\lambda (v: 
-T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) w) v))) x1 x3 (refl_equal T 
-(THead (Bind Abst) w x1)) H11 (ty3_conv g (CHead c (Bind Abst) w) u x2 H12 x1 
-x5 H20 (H19 Abst w)) H21) x0 H_y)))))) (pc3_gen_abst c x0 w x5 u H14))))))))) 
-(ty3_gen_bind g Abst c x0 x1 (THead (Bind Abst) w u) H8))))))))) 
-(ty3_gen_bind g Abst c w u x H9)))) (ty3_correct g c (THead (Bind Abst) x0 
-x1) (THead (Bind Abst) w u) H8)) t H5))))))) H4)) (\lambda (H4: (ex nat 
-(\lambda (n: nat).(eq T t (TSort n))))).(ex_ind nat (\lambda (n: nat).(eq T t 
-(TSort n))) (ex4_2 T T (\lambda (v: T).(\lambda (_: T).(eq T t (THead (Bind 
-Abst) w v)))) (\lambda (_: T).(\lambda (w0: T).(ty3 g c w w0))) (\lambda (v: 
-T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) w) v u))) (\lambda (v: 
-T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) w) v)))) (\lambda (x: 
-nat).(\lambda (H5: (eq T t (TSort x))).(let H6 \def (eq_ind T t (\lambda (t0: 
-T).(ty3 g c t0 (THead (Bind Abst) w u))) H (TSort x) H5) in (eq_ind_r T 
-(TSort x) (\lambda (t0: T).(ex4_2 T T (\lambda (v: T).(\lambda (_: T).(eq T 
-t0 (THead (Bind Abst) w v)))) (\lambda (_: T).(\lambda (w0: T).(ty3 g c w 
-w0))) (\lambda (v: T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) w) v u))) 
-(\lambda (v: T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) w) v))))) 
-(pc3_gen_sort_abst c w u (next g x) (ty3_gen_sort g c (THead (Bind Abst) w u) 
-x H6) (ex4_2 T T (\lambda (v: T).(\lambda (_: T).(eq T (TSort x) (THead (Bind 
-Abst) w v)))) (\lambda (_: T).(\lambda (w0: T).(ty3 g c w w0))) (\lambda (v: 
-T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) w) v u))) (\lambda (v: 
-T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) w) v))))) t H5)))) H4)) (\lambda 
-(H4: (ex3_2 TList nat (\lambda (ws: TList).(\lambda (i: nat).(eq T t (THeads 
-(Flat Appl) ws (TLRef i))))) (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c 
-ws))) (\lambda (_: TList).(\lambda (i: nat).(nf2 c (TLRef i)))))).(ex3_2_ind 
-TList nat (\lambda (ws: TList).(\lambda (i: nat).(eq T t (THeads (Flat Appl) 
-ws (TLRef i))))) (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c ws))) 
-(\lambda (_: TList).(\lambda (i: nat).(nf2 c (TLRef i)))) (ex4_2 T T (\lambda 
+T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) w) v)))) (\lambda (H16: (pc3 c 
+x0 w)).(\lambda (H17: ((\forall (b: B).(\forall (u0: T).(pc3 (CHead c (Bind 
+b) u0) x4 u))))).(let H_y \def (pc3_nf2 c x0 w H16 H6 H1) in (let H18 \def 
+(eq_ind T x0 (\lambda (t0: T).(ty3 g (CHead c (Bind Abst) t0) x1 x4)) H15 w 
+H_y) in (let H19 \def (eq_ind T x0 (\lambda (t0: T).(nf2 (CHead c (Bind Abst) 
+t0) x1)) H7 w H_y) in (eq_ind_r T w (\lambda (t0: T).(ex4_2 T T (\lambda (v: 
+T).(\lambda (_: T).(eq T (THead (Bind Abst) t0 x1) (THead (Bind Abst) w v)))) 
+(\lambda (_: T).(\lambda (w0: T).(ty3 g c w w0))) (\lambda (v: T).(\lambda 
+(_: T).(ty3 g (CHead c (Bind Abst) w) v u))) (\lambda (v: T).(\lambda (_: 
+T).(nf2 (CHead c (Bind Abst) w) v))))) (ex4_2_intro T T (\lambda (v: 
+T).(\lambda (_: T).(eq T (THead (Bind Abst) w x1) (THead (Bind Abst) w v)))) 
+(\lambda (_: T).(\lambda (w0: T).(ty3 g c w w0))) (\lambda (v: T).(\lambda 
+(_: T).(ty3 g (CHead c (Bind Abst) w) v u))) (\lambda (v: T).(\lambda (_: 
+T).(nf2 (CHead c (Bind Abst) w) v))) x1 x3 (refl_equal T (THead (Bind Abst) w 
+x1)) H11 (ty3_conv g (CHead c (Bind Abst) w) u x2 H12 x1 x4 H18 (H17 Abst w)) 
+H19) x0 H_y)))))) (pc3_gen_abst c x0 w x4 u H13))))))) (ty3_gen_bind g Abst c 
+x0 x1 (THead (Bind Abst) w u) H8))))))) (ty3_gen_bind g Abst c w u x H9)))) 
+(ty3_correct g c (THead (Bind Abst) x0 x1) (THead (Bind Abst) w u) H8)) t 
+H5))))))) H4)) (\lambda (H4: (ex nat (\lambda (n: nat).(eq T t (TSort 
+n))))).(ex_ind nat (\lambda (n: nat).(eq T t (TSort n))) (ex4_2 T T (\lambda 
 (v: T).(\lambda (_: T).(eq T t (THead (Bind Abst) w v)))) (\lambda (_: 
 T).(\lambda (w0: T).(ty3 g c w w0))) (\lambda (v: T).(\lambda (_: T).(ty3 g 
 (CHead c (Bind Abst) w) v u))) (\lambda (v: T).(\lambda (_: T).(nf2 (CHead c 
-(Bind Abst) w) v)))) (\lambda (x0: TList).(\lambda (x1: nat).(\lambda (H5: 
-(eq T t (THeads (Flat Appl) x0 (TLRef x1)))).(\lambda (_: (nfs2 c 
-x0)).(\lambda (H7: (nf2 c (TLRef x1))).(let H8 \def (eq_ind T t (\lambda (t0: 
-T).(ty3 g c t0 (THead (Bind Abst) w u))) H (THeads (Flat Appl) x0 (TLRef x1)) 
-H5) in (eq_ind_r T (THeads (Flat Appl) x0 (TLRef x1)) (\lambda (t0: T).(ex4_2 
-T T (\lambda (v: T).(\lambda (_: T).(eq T t0 (THead (Bind Abst) w v)))) 
-(\lambda (_: T).(\lambda (w0: T).(ty3 g c w w0))) (\lambda (v: T).(\lambda 
-(_: T).(ty3 g (CHead c (Bind Abst) w) v u))) (\lambda (v: T).(\lambda (_: 
-T).(nf2 (CHead c (Bind Abst) w) v))))) (let H9 \def H2 in ((let H10 \def H8 
-in (unintro T u (\lambda (t0: T).((ty3 g c (THeads (Flat Appl) x0 (TLRef x1)) 
-(THead (Bind Abst) w t0)) \to ((ty3_nf2_inv_abst_premise c w t0) \to (ex4_2 T 
-T (\lambda (v: T).(\lambda (_: T).(eq T (THeads (Flat Appl) x0 (TLRef x1)) 
+(Bind Abst) w) v)))) (\lambda (x: nat).(\lambda (H5: (eq T t (TSort x))).(let 
+H6 \def (eq_ind T t (\lambda (t0: T).(ty3 g c t0 (THead (Bind Abst) w u))) H 
+(TSort x) H5) in (eq_ind_r T (TSort x) (\lambda (t0: T).(ex4_2 T T (\lambda 
+(v: T).(\lambda (_: T).(eq T t0 (THead (Bind Abst) w v)))) (\lambda (_: 
+T).(\lambda (w0: T).(ty3 g c w w0))) (\lambda (v: T).(\lambda (_: T).(ty3 g 
+(CHead c (Bind Abst) w) v u))) (\lambda (v: T).(\lambda (_: T).(nf2 (CHead c 
+(Bind Abst) w) v))))) (pc3_gen_sort_abst c w u (next g x) (ty3_gen_sort g c 
+(THead (Bind Abst) w u) x H6) (ex4_2 T T (\lambda (v: T).(\lambda (_: T).(eq 
+T (TSort x) (THead (Bind Abst) w v)))) (\lambda (_: T).(\lambda (w0: T).(ty3 
+g c w w0))) (\lambda (v: T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) w) v 
+u))) (\lambda (v: T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) w) v))))) t 
+H5)))) H4)) (\lambda (H4: (ex3_2 TList nat (\lambda (ws: TList).(\lambda (i: 
+nat).(eq T t (THeads (Flat Appl) ws (TLRef i))))) (\lambda (ws: 
+TList).(\lambda (_: nat).(nfs2 c ws))) (\lambda (_: TList).(\lambda (i: 
+nat).(nf2 c (TLRef i)))))).(ex3_2_ind TList nat (\lambda (ws: TList).(\lambda 
+(i: nat).(eq T t (THeads (Flat Appl) ws (TLRef i))))) (\lambda (ws: 
+TList).(\lambda (_: nat).(nfs2 c ws))) (\lambda (_: TList).(\lambda (i: 
+nat).(nf2 c (TLRef i)))) (ex4_2 T T (\lambda (v: T).(\lambda (_: T).(eq T t 
 (THead (Bind Abst) w v)))) (\lambda (_: T).(\lambda (w0: T).(ty3 g c w w0))) 
-(\lambda (v: T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) w) v t0))) 
-(\lambda (v: T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) w) v))))))) 
-(unintro T w (\lambda (t0: T).(\forall (x: T).((ty3 g c (THeads (Flat Appl) 
-x0 (TLRef x1)) (THead (Bind Abst) t0 x)) \to ((ty3_nf2_inv_abst_premise c t0 
-x) \to (ex4_2 T T (\lambda (v: T).(\lambda (_: T).(eq T (THeads (Flat Appl) 
-x0 (TLRef x1)) (THead (Bind Abst) t0 v)))) (\lambda (_: T).(\lambda (w0: 
-T).(ty3 g c t0 w0))) (\lambda (v: T).(\lambda (_: T).(ty3 g (CHead c (Bind 
-Abst) t0) v x))) (\lambda (v: T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) 
-t0) v)))))))) (TList_ind (\lambda (t0: TList).(\forall (x: T).(\forall (x2: 
-T).((ty3 g c (THeads (Flat Appl) t0 (TLRef x1)) (THead (Bind Abst) x x2)) \to 
+(\lambda (v: T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) w) v u))) 
+(\lambda (v: T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) w) v)))) (\lambda 
+(x0: TList).(\lambda (x1: nat).(\lambda (H5: (eq T t (THeads (Flat Appl) x0 
+(TLRef x1)))).(\lambda (_: (nfs2 c x0)).(\lambda (H7: (nf2 c (TLRef 
+x1))).(let H8 \def (eq_ind T t (\lambda (t0: T).(ty3 g c t0 (THead (Bind 
+Abst) w u))) H (THeads (Flat Appl) x0 (TLRef x1)) H5) in (eq_ind_r T (THeads 
+(Flat Appl) x0 (TLRef x1)) (\lambda (t0: T).(ex4_2 T T (\lambda (v: 
+T).(\lambda (_: T).(eq T t0 (THead (Bind Abst) w v)))) (\lambda (_: 
+T).(\lambda (w0: T).(ty3 g c w w0))) (\lambda (v: T).(\lambda (_: T).(ty3 g 
+(CHead c (Bind Abst) w) v u))) (\lambda (v: T).(\lambda (_: T).(nf2 (CHead c 
+(Bind Abst) w) v))))) (let H9 \def H2 in ((let H10 \def H8 in (unintro T u 
+(\lambda (t0: T).((ty3 g c (THeads (Flat Appl) x0 (TLRef x1)) (THead (Bind 
+Abst) w t0)) \to ((ty3_nf2_inv_abst_premise c w t0) \to (ex4_2 T T (\lambda 
+(v: T).(\lambda (_: T).(eq T (THeads (Flat Appl) x0 (TLRef x1)) (THead (Bind 
+Abst) w v)))) (\lambda (_: T).(\lambda (w0: T).(ty3 g c w w0))) (\lambda (v: 
+T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) w) v t0))) (\lambda (v: 
+T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) w) v))))))) (unintro T w 
+(\lambda (t0: T).(\forall (x: T).((ty3 g c (THeads (Flat Appl) x0 (TLRef x1)) 
+(THead (Bind Abst) t0 x)) \to ((ty3_nf2_inv_abst_premise c t0 x) \to (ex4_2 T 
+T (\lambda (v: T).(\lambda (_: T).(eq T (THeads (Flat Appl) x0 (TLRef x1)) 
+(THead (Bind Abst) t0 v)))) (\lambda (_: T).(\lambda (w0: T).(ty3 g c t0 
+w0))) (\lambda (v: T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) t0) v x))) 
+(\lambda (v: T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) t0) v)))))))) 
+(TList_ind (\lambda (t0: TList).(\forall (x: T).(\forall (x2: T).((ty3 g c 
+(THeads (Flat Appl) t0 (TLRef x1)) (THead (Bind Abst) x x2)) \to 
 ((ty3_nf2_inv_abst_premise c x x2) \to (ex4_2 T T (\lambda (v: T).(\lambda 
 (_: T).(eq T (THeads (Flat Appl) t0 (TLRef x1)) (THead (Bind Abst) x v)))) 
 (\lambda (_: T).(\lambda (w0: T).(ty3 g c x w0))) (\lambda (v: T).(\lambda