-B).(\forall (u: T).(pr2 (CHead (CSort O) (Bind b) u) z1 t3))))))) (eq T
-(THead (Flat Appl) (TSort O) (TSort O)) t2) (\lambda (x0: T).(\lambda (x1:
-T).(\lambda (x2: T).(\lambda (x3: T).(\lambda (H2: (eq T (TSort O) (THead
-(Bind Abst) x0 x1))).(\lambda (H3: (eq T t2 (THead (Bind Abbr) x2
-x3))).(\lambda (H4: (pr2 (CSort O) (TSort O) x2)).(\lambda (_: ((\forall (b:
-B).(\forall (u: T).(pr2 (CHead (CSort O) (Bind b) u) x1 x3))))).(let H6 \def
-(eq_ind T x2 (\lambda (t: T).(eq T t2 (THead (Bind Abbr) t x3))) H3 (TSort O)
-(pr2_gen_sort (CSort O) x2 O H4)) in (eq_ind_r T (THead (Bind Abbr) (TSort O)
-x3) (\lambda (t: T).(eq T (THead (Flat Appl) (TSort O) (TSort O)) t)) (let H7
-\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).(\forall (u: T).(let TMP_24 \def (CSort O) in (let TMP_25 \def (Bind b) in
+(let TMP_26 \def (CHead TMP_24 TMP_25 u) in (pr2 TMP_26 z1 t3)))))))))) in
+(let TMP_28 \def (ex4_4 T T T T TMP_17 TMP_20 TMP_23 TMP_27) in (let TMP_30
+\def (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
+(_: T).(\lambda (_: T).(let TMP_29 \def (eq B b Abst) in (not TMP_29))))))))
+in (let TMP_34 \def (\lambda (b: B).(\lambda (y1: T).(\lambda (z1:
+T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(let TMP_31 \def (TSort O)
+in (let TMP_32 \def (Bind b) in (let TMP_33 \def (THead TMP_32 y1 z1) in (eq
+T TMP_31 TMP_33)))))))))) in (let TMP_41 \def (\lambda (b: B).(\lambda (_:
+T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(let
+TMP_35 \def (Bind b) in (let TMP_36 \def (Flat Appl) in (let TMP_37 \def (S
+O) in (let TMP_38 \def (lift TMP_37 O u2) in (let TMP_39 \def (THead TMP_36
+TMP_38 z2) in (let TMP_40 \def (THead TMP_35 y2 TMP_39) in (eq T t2
+TMP_40))))))))))))) in (let TMP_44 \def (\lambda (_: B).(\lambda (_:
+T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(let
+TMP_42 \def (CSort O) in (let TMP_43 \def (TSort O) in (pr2 TMP_42 TMP_43
+u2))))))))) in (let TMP_46 \def (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
+T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(let TMP_45 \def (CSort
+O) in (pr2 TMP_45 y1 y2)))))))) in (let TMP_50 \def (\lambda (b: B).(\lambda
+(_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2:
+T).(let TMP_47 \def (CSort O) in (let TMP_48 \def (Bind b) in (let TMP_49
+\def (CHead TMP_47 TMP_48 y2) in (pr2 TMP_49 z1 z2)))))))))) in (let TMP_51
+\def (ex6_6 B T T T T T TMP_30 TMP_34 TMP_41 TMP_44 TMP_46 TMP_50) in (let
+TMP_52 \def (Flat Appl) in (let TMP_53 \def (TSort O) in (let TMP_54 \def
+(TSort O) in (let TMP_55 \def (THead TMP_52 TMP_53 TMP_54) in (let TMP_56
+\def (eq T TMP_55 t2) in (let TMP_99 \def (\lambda (H1: (ex3_2 T T (\lambda
+(u2: T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 t3)))) (\lambda (u2:
+T).(\lambda (_: T).(pr2 (CSort O) (TSort O) u2))) (\lambda (_: T).(\lambda
+(t3: T).(pr2 (CSort O) (TSort O) t3))))).(let TMP_59 \def (\lambda (u2:
+T).(\lambda (t3: T).(let TMP_57 \def (Flat Appl) in (let TMP_58 \def (THead
+TMP_57 u2 t3) in (eq T t2 TMP_58))))) in (let TMP_62 \def (\lambda (u2:
+T).(\lambda (_: T).(let TMP_60 \def (CSort O) in (let TMP_61 \def (TSort O)
+in (pr2 TMP_60 TMP_61 u2))))) in (let TMP_65 \def (\lambda (_: T).(\lambda
+(t3: T).(let TMP_63 \def (CSort O) in (let TMP_64 \def (TSort O) in (pr2
+TMP_63 TMP_64 t3))))) in (let TMP_66 \def (Flat Appl) in (let TMP_67 \def
+(TSort O) in (let TMP_68 \def (TSort O) in (let TMP_69 \def (THead TMP_66
+TMP_67 TMP_68) in (let TMP_70 \def (eq T TMP_69 t2) in (let TMP_98 \def
+(\lambda (x0: T).(\lambda (x1: T).(\lambda (H2: (eq T t2 (THead (Flat Appl)
+x0 x1))).(\lambda (H3: (pr2 (CSort O) (TSort O) x0)).(\lambda (H4: (pr2
+(CSort O) (TSort O) x1)).(let TMP_73 \def (\lambda (t: T).(let TMP_71 \def
+(Flat Appl) in (let TMP_72 \def (THead TMP_71 x0 t) in (eq T t2 TMP_72)))) in
+(let TMP_74 \def (TSort O) in (let TMP_75 \def (CSort O) in (let TMP_76 \def
+(pr2_gen_sort TMP_75 x1 O H4) in (let H5 \def (eq_ind T x1 TMP_73 H2 TMP_74
+TMP_76) in (let TMP_80 \def (\lambda (t: T).(let TMP_77 \def (Flat Appl) in
+(let TMP_78 \def (TSort O) in (let TMP_79 \def (THead TMP_77 t TMP_78) in (eq
+T t2 TMP_79))))) in (let TMP_81 \def (TSort O) in (let TMP_82 \def (CSort O)
+in (let TMP_83 \def (pr2_gen_sort TMP_82 x0 O H3) in (let H6 \def (eq_ind T
+x0 TMP_80 H5 TMP_81 TMP_83) in (let TMP_84 \def (Flat Appl) in (let TMP_85
+\def (TSort O) in (let TMP_86 \def (TSort O) in (let TMP_87 \def (THead
+TMP_84 TMP_85 TMP_86) in (let TMP_92 \def (\lambda (t: T).(let TMP_88 \def
+(Flat Appl) in (let TMP_89 \def (TSort O) in (let TMP_90 \def (TSort O) in
+(let TMP_91 \def (THead TMP_88 TMP_89 TMP_90) in (eq T TMP_91 t)))))) in (let
+TMP_93 \def (Flat Appl) in (let TMP_94 \def (TSort O) in (let TMP_95 \def
+(TSort O) in (let TMP_96 \def (THead TMP_93 TMP_94 TMP_95) in (let TMP_97
+\def (refl_equal T TMP_96) in (eq_ind_r T TMP_87 TMP_92 TMP_97 t2
+H6)))))))))))))))))))))))))) in (ex3_2_ind T T TMP_59 TMP_62 TMP_65 TMP_70
+TMP_98 H1))))))))))) in (let TMP_147 \def (\lambda (H1: (ex4_4 T T T T
+(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T
+(TSort O) (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_:
+T).(\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3))))))
+(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 (CSort
+O) (TSort O) u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
+T).(\lambda (t3: T).(\forall (b: B).(\forall (u: T).(pr2 (CHead (CSort O)
+(Bind b) u) z1 t3))))))))).(let TMP_103 \def (\lambda (y1: T).(\lambda (z1:
+T).(\lambda (_: T).(\lambda (_: T).(let TMP_100 \def (TSort O) in (let
+TMP_101 \def (Bind Abst) in (let TMP_102 \def (THead TMP_101 y1 z1) in (eq T
+TMP_100 TMP_102)))))))) in (let TMP_106 \def (\lambda (_: T).(\lambda (_:
+T).(\lambda (u2: T).(\lambda (t3: T).(let TMP_104 \def (Bind Abbr) in (let
+TMP_105 \def (THead TMP_104 u2 t3) in (eq T t2 TMP_105))))))) in (let TMP_109
+\def (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(let
+TMP_107 \def (CSort O) in (let TMP_108 \def (TSort O) in (pr2 TMP_107 TMP_108
+u2))))))) in (let TMP_113 \def (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
+T).(\lambda (t3: T).(\forall (b: B).(\forall (u: T).(let TMP_110 \def (CSort
+O) in (let TMP_111 \def (Bind b) in (let TMP_112 \def (CHead TMP_110 TMP_111
+u) in (pr2 TMP_112 z1 t3)))))))))) in (let TMP_114 \def (Flat Appl) in (let
+TMP_115 \def (TSort O) in (let TMP_116 \def (TSort O) in (let TMP_117 \def
+(THead TMP_114 TMP_115 TMP_116) in (let TMP_118 \def (eq T TMP_117 t2) in
+(let TMP_146 \def (\lambda (x0: T).(\lambda (x1: T).(\lambda (x2: T).(\lambda
+(x3: T).(\lambda (H2: (eq T (TSort O) (THead (Bind Abst) x0 x1))).(\lambda
+(H3: (eq T t2 (THead (Bind Abbr) x2 x3))).(\lambda (H4: (pr2 (CSort O) (TSort
+O) x2)).(\lambda (_: ((\forall (b: B).(\forall (u: T).(pr2 (CHead (CSort O)
+(Bind b) u) x1 x3))))).(let TMP_121 \def (\lambda (t: T).(let TMP_119 \def
+(Bind Abbr) in (let TMP_120 \def (THead TMP_119 t x3) in (eq T t2 TMP_120))))
+in (let TMP_122 \def (TSort O) in (let TMP_123 \def (CSort O) in (let TMP_124
+\def (pr2_gen_sort TMP_123 x2 O H4) in (let H6 \def (eq_ind T x2 TMP_121 H3
+TMP_122 TMP_124) in (let TMP_125 \def (Bind Abbr) in (let TMP_126 \def (TSort
+O) in (let TMP_127 \def (THead TMP_125 TMP_126 x3) in (let TMP_132 \def
+(\lambda (t: T).(let TMP_128 \def (Flat Appl) in (let TMP_129 \def (TSort O)
+in (let TMP_130 \def (TSort O) in (let TMP_131 \def (THead TMP_128 TMP_129
+TMP_130) in (eq T TMP_131 t)))))) in (let TMP_133 \def (TSort O) in (let
+TMP_134 \def (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow True |
+(TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow False])) in (let
+TMP_135 \def (Bind Abst) in (let TMP_136 \def (THead TMP_135 x0 x1) in (let
+H7 \def (eq_ind T TMP_133 TMP_134 I TMP_136 H2) in (let TMP_137 \def (Flat
+Appl) in (let TMP_138 \def (TSort O) in (let TMP_139 \def (TSort O) in (let
+TMP_140 \def (THead TMP_137 TMP_138 TMP_139) in (let TMP_141 \def (Bind Abbr)
+in (let TMP_142 \def (TSort O) in (let TMP_143 \def (THead TMP_141 TMP_142
+x3) in (let TMP_144 \def (eq T TMP_140 TMP_143) in (let TMP_145 \def
+(False_ind TMP_144 H7) in (eq_ind_r T TMP_127 TMP_132 TMP_145 t2
+H6)))))))))))))))))))))))))))))))) in (ex4_4_ind T T T T TMP_103 TMP_106
+TMP_109 TMP_113 TMP_118 TMP_146 H1)))))))))))) in (let TMP_215 \def (\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))))))))).(let TMP_149 \def (\lambda (b: