(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/nf2".
+include "LambdaDelta-1/ty3/arity.ma".
-include "ty3/arity.ma".
+include "LambdaDelta-1/pc3/nf2.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))
(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
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:
-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:
+(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)).(land_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))))) 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