-nat).(nf2 c0 (TLRef i))))))) with []) in H9)))) (\lambda (_: (not (eq B Void
-Abst))).(\lambda (H7: (arity g (CHead c0 (Bind Void) u) t0 a2)).(\lambda (H8:
-(nf2 c0 (THead (Bind Void) u t0))).(let H9 \def (arity_gen_cvoid g (CHead c0
-(Bind Void) u) t0 a2 H7 c0 u O (getl_refl Void c0 u)) in (ex_ind T (\lambda
-(v: T).(eq T t0 (lift (S O) O v))) (or3 (ex3_2 T T (\lambda (w: T).(\lambda
-(u0: T).(eq T (THead (Bind Void) 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 (Bind
-Void) u t0) (TSort n)))) (ex3_2 TList nat (\lambda (ws: TList).(\lambda (i:
-nat).(eq T (THead (Bind Void) 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 (x: T).(\lambda
-(H10: (eq T t0 (lift (S O) O x))).(let H11 \def (eq_ind T t0 (\lambda (t1:
-T).(nf2 c0 (THead (Bind Void) u t1))) H8 (lift (S O) O x) H10) in (eq_ind_r T
-(lift (S O) O x) (\lambda (t1: T).(or3 (ex3_2 T T (\lambda (w: T).(\lambda
-(u0: T).(eq T (THead (Bind Void) u t1) (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 (Bind
-Void) u t1) (TSort n)))) (ex3_2 TList nat (\lambda (ws: TList).(\lambda (i:
-nat).(eq T (THead (Bind Void) u t1) (THeads (Flat Appl) ws (TLRef i)))))
-(\lambda (ws: TList).(\lambda (_: nat).(nfs2 c0 ws))) (\lambda (_:
-TList).(\lambda (i: nat).(nf2 c0 (TLRef i))))))) (nf2_gen_void c0 u x H11
-(or3 (ex3_2 T T (\lambda (w: T).(\lambda (u0: T).(eq T (THead (Bind Void) u
-(lift (S O) O x)) (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 (Bind Void) u (lift (S O) O
-x)) (TSort n)))) (ex3_2 TList nat (\lambda (ws: TList).(\lambda (i: nat).(eq
-T (THead (Bind Void) u (lift (S O) O x)) (THeads (Flat Appl) ws (TLRef i)))))
-(\lambda (ws: TList).(\lambda (_: nat).(nfs2 c0 ws))) (\lambda (_:
-TList).(\lambda (i: nat).(nf2 c0 (TLRef i))))))) t0 H10)))) H9))))) b H0 H3
-H5))))))))))))) (\lambda (c0: C).(\lambda (u: T).(\lambda (a1: A).(\lambda
-(_: (arity g c0 u (asucc g a1))).(\lambda (_: (((nf2 c0 u) \to (or3 (ex3_2 T
-T (\lambda (w: T).(\lambda (u0: T).(eq T u (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 u
-(TSort n)))) (ex3_2 TList nat (\lambda (ws: TList).(\lambda (i: nat).(eq T u
-(THeads (Flat Appl) ws (TLRef i))))) (\lambda (ws: TList).(\lambda (_:
-nat).(nfs2 c0 ws))) (\lambda (_: TList).(\lambda (i: nat).(nf2 c0 (TLRef
-i))))))))).(\lambda (t0: T).(\lambda (a2: A).(\lambda (_: (arity g (CHead c0
-(Bind Abst) u) t0 a2)).(\lambda (_: (((nf2 (CHead c0 (Bind Abst) u) t0) \to
-(or3 (ex3_2 T T (\lambda (w: T).(\lambda (u0: T).(eq T t0 (THead (Bind Abst)
-w u0)))) (\lambda (w: T).(\lambda (_: T).(nf2 (CHead c0 (Bind Abst) u) w)))
-(\lambda (w: T).(\lambda (u0: T).(nf2 (CHead (CHead c0 (Bind Abst) u) (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 (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 (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
-c0 (Bind Abst) w) u0)))) (ex nat (\lambda (n: nat).(eq T (THead (Bind Abst) u
-t0) (TSort n)))) (ex3_2 TList nat (\lambda (ws: TList).(\lambda (i: nat).(eq
-T (THead (Bind Abst) u t0) (THeads (Flat Appl) ws (TLRef i))))) (\lambda (ws:
-TList).(\lambda (_: nat).(nfs2 c0 ws))) (\lambda (_: TList).(\lambda (i: