-(\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 (_: