-\def (eq_ind T (TSort O) (\lambda (ee: T).(match ee in T return (\lambda (_:
-T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False |
-(THead _ _ _) \Rightarrow False])) I (THead (Bind Abst) x0 x1) H2) in
-(False_ind (eq T (THead (Flat Appl) (TSort O) (TSort O)) (THead (Bind Abbr)
-(TSort O) x3)) H7)) t2 H6)))))))))) H1)) (\lambda (H1: (ex6_6 B T T T T T
-(\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
-T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
-T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T
-(TSort O) (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_:
-T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T
-t2 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)))))))))
-(\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2:
-T).(\lambda (_: T).(pr2 (CSort O) (TSort O) u2))))))) (\lambda (_:
-B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
-(y2: T).(pr2 (CSort O) y1 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda
-(z1: T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead (CSort
-O) (Bind b) y2) z1 z2))))))))).(ex6_6_ind B T T T T T (\lambda (b:
-B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
-(_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda
-(z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T (TSort O)
-(THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
+\def (eq_ind T (TSort O) (\lambda (ee: T).(match ee with [(TSort _)
+\Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
+False])) I (THead (Bind Abst) x0 x1) H2) in (False_ind (eq T (THead (Flat
+Appl) (TSort O) (TSort O)) (THead (Bind Abbr) (TSort O) x3)) H7)) t2
+H6)))))))))) H1)) (\lambda (H1: (ex6_6 B T T T T T (\lambda (b: B).(\lambda
+(_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not
+(eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda (z1:
+T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T (TSort O) (THead
+(Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
+T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T t2 (THead (Bind
+b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_:
+B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
+(_: T).(pr2 (CSort O) (TSort O) u2))))))) (\lambda (_: B).(\lambda (y1:
+T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2
+(CSort O) y1 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1:
+T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead (CSort O)
+(Bind b) y2) z1 z2))))))))).(ex6_6_ind B T T T T T (\lambda (b: B).(\lambda
+(_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not
+(eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda (z1:
+T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T (TSort O) (THead
+(Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_: