-(CHead c0 (Bind b0) u) (CHead c1 (Bind b) v))).(let TMP_53 \def (\lambda (e:
-C).(match e with [(CSort _) \Rightarrow c0 | (CHead c _ _) \Rightarrow c]))
-in (let TMP_54 \def (Bind b0) in (let TMP_55 \def (CHead c0 TMP_54 u) in (let
-TMP_56 \def (Bind b) in (let TMP_57 \def (CHead c1 TMP_56 v) in (let H5 \def
-(f_equal C C TMP_53 TMP_55 TMP_57 H4) in (let TMP_58 \def (\lambda (e:
-C).(match e with [(CSort _) \Rightarrow b0 | (CHead _ k _) \Rightarrow (match
-k with [(Bind b1) \Rightarrow b1 | (Flat _) \Rightarrow b0])])) in (let
-TMP_59 \def (Bind b0) in (let TMP_60 \def (CHead c0 TMP_59 u) in (let TMP_61
-\def (Bind b) in (let TMP_62 \def (CHead c1 TMP_61 v) in (let H6 \def
-(f_equal C B TMP_58 TMP_60 TMP_62 H4) in (let TMP_63 \def (\lambda (e:
-C).(match e with [(CSort _) \Rightarrow u | (CHead _ _ t0) \Rightarrow t0]))
-in (let TMP_64 \def (Bind b0) in (let TMP_65 \def (CHead c0 TMP_64 u) in (let
-TMP_66 \def (Bind b) in (let TMP_67 \def (CHead c1 TMP_66 v) in (let H7 \def
-(f_equal C T TMP_63 TMP_65 TMP_67 H4) in (let TMP_151 \def (\lambda (H8: (eq
-B b0 b)).(\lambda (H9: (eq C c0 c1)).(let TMP_85 \def (\lambda (b1: B).(let
-TMP_72 \def (\lambda (c3: C).(\lambda (_: T).(let TMP_68 \def (Bind b1) in
-(let TMP_69 \def (CHead c2 TMP_68 u) in (let TMP_70 \def (Bind b) in (let
-TMP_71 \def (CHead c3 TMP_70 v) in (eq C TMP_69 TMP_71))))))) in (let TMP_73
-\def (\lambda (c3: C).(\lambda (_: T).(wf3 g c1 c3))) in (let TMP_74 \def
-(\lambda (_: C).(\lambda (w: T).(ty3 g c1 v w))) in (let TMP_75 \def (ex3_2 C
-T TMP_72 TMP_73 TMP_74) in (let TMP_81 \def (\lambda (c3: C).(let TMP_76 \def
-(Bind b1) in (let TMP_77 \def (CHead c2 TMP_76 u) in (let TMP_78 \def (Bind
-Void) in (let TMP_79 \def (TSort O) in (let TMP_80 \def (CHead c3 TMP_78
-TMP_79) in (eq C TMP_77 TMP_80))))))) in (let TMP_82 \def (\lambda (c3:
-C).(wf3 g c1 c3)) in (let TMP_83 \def (\lambda (_: C).(\forall (w: T).((ty3 g
-c1 v w) \to False))) in (let TMP_84 \def (ex3 C TMP_81 TMP_82 TMP_83) in (or
-TMP_75 TMP_84)))))))))) in (let TMP_86 \def (\lambda (t0: T).(ty3 g c0 t0 t))
-in (let H10 \def (eq_ind T u TMP_86 H3 v H7) in (let TMP_104 \def (\lambda
-(t0: T).(let TMP_91 \def (\lambda (c3: C).(\lambda (_: T).(let TMP_87 \def
-(Bind b) in (let TMP_88 \def (CHead c2 TMP_87 t0) in (let TMP_89 \def (Bind
-b) in (let TMP_90 \def (CHead c3 TMP_89 v) in (eq C TMP_88 TMP_90))))))) in
-(let TMP_92 \def (\lambda (c3: C).(\lambda (_: T).(wf3 g c1 c3))) in (let
-TMP_93 \def (\lambda (_: C).(\lambda (w: T).(ty3 g c1 v w))) in (let TMP_94
-\def (ex3_2 C T TMP_91 TMP_92 TMP_93) in (let TMP_100 \def (\lambda (c3:
-C).(let TMP_95 \def (Bind b) in (let TMP_96 \def (CHead c2 TMP_95 t0) in (let
-TMP_97 \def (Bind Void) in (let TMP_98 \def (TSort O) in (let TMP_99 \def
-(CHead c3 TMP_97 TMP_98) in (eq C TMP_96 TMP_99))))))) in (let TMP_101 \def
-(\lambda (c3: C).(wf3 g c1 c3)) in (let TMP_102 \def (\lambda (_: C).(\forall
-(w: T).((ty3 g c1 v w) \to False))) in (let TMP_103 \def (ex3 C TMP_100
-TMP_101 TMP_102) in (or TMP_94 TMP_103)))))))))) in (let TMP_105 \def
-(\lambda (c: C).(ty3 g c v t)) in (let H11 \def (eq_ind C c0 TMP_105 H10 c1
-H9) in (let TMP_119 \def (\lambda (c: C).((eq C c (CHead c1 (Bind b) v)) \to
-(let TMP_108 \def (\lambda (c3: C).(\lambda (_: T).(let TMP_106 \def (Bind b)
-in (let TMP_107 \def (CHead c3 TMP_106 v) in (eq C c2 TMP_107))))) in (let
-TMP_109 \def (\lambda (c3: C).(\lambda (_: T).(wf3 g c1 c3))) in (let TMP_110
-\def (\lambda (_: C).(\lambda (w: T).(ty3 g c1 v w))) in (let TMP_111 \def
-(ex3_2 C T TMP_108 TMP_109 TMP_110) in (let TMP_115 \def (\lambda (c3:
-C).(let TMP_112 \def (Bind Void) in (let TMP_113 \def (TSort O) in (let
-TMP_114 \def (CHead c3 TMP_112 TMP_113) in (eq C c2 TMP_114))))) in (let
-TMP_116 \def (\lambda (c3: C).(wf3 g c1 c3)) in (let TMP_117 \def (\lambda
-(_: C).(\forall (w: T).((ty3 g c1 v w) \to False))) in (let TMP_118 \def (ex3
-C TMP_115 TMP_116 TMP_117) in (or TMP_111 TMP_118))))))))))) in (let H12 \def
-(eq_ind C c0 TMP_119 H2 c1 H9) in (let TMP_120 \def (\lambda (c: C).(wf3 g c
-c2)) in (let H13 \def (eq_ind C c0 TMP_120 H1 c1 H9) in (let TMP_125 \def
-(\lambda (c3: C).(\lambda (_: T).(let TMP_121 \def (Bind b) in (let TMP_122
-\def (CHead c2 TMP_121 v) in (let TMP_123 \def (Bind b) in (let TMP_124 \def
-(CHead c3 TMP_123 v) in (eq C TMP_122 TMP_124))))))) in (let TMP_126 \def
-(\lambda (c3: C).(\lambda (_: T).(wf3 g c1 c3))) in (let TMP_127 \def
-(\lambda (_: C).(\lambda (w: T).(ty3 g c1 v w))) in (let TMP_128 \def (ex3_2
-C T TMP_125 TMP_126 TMP_127) in (let TMP_134 \def (\lambda (c3: C).(let
-TMP_129 \def (Bind b) in (let TMP_130 \def (CHead c2 TMP_129 v) in (let
-TMP_131 \def (Bind Void) in (let TMP_132 \def (TSort O) in (let TMP_133 \def
-(CHead c3 TMP_131 TMP_132) in (eq C TMP_130 TMP_133))))))) in (let TMP_135
-\def (\lambda (c3: C).(wf3 g c1 c3)) in (let TMP_136 \def (\lambda (_:
-C).(\forall (w: T).((ty3 g c1 v w) \to False))) in (let TMP_137 \def (ex3 C
-TMP_134 TMP_135 TMP_136) in (let TMP_142 \def (\lambda (c3: C).(\lambda (_:
-T).(let TMP_138 \def (Bind b) in (let TMP_139 \def (CHead c2 TMP_138 v) in
-(let TMP_140 \def (Bind b) in (let TMP_141 \def (CHead c3 TMP_140 v) in (eq C
-TMP_139 TMP_141))))))) in (let TMP_143 \def (\lambda (c3: C).(\lambda (_:
-T).(wf3 g c1 c3))) in (let TMP_144 \def (\lambda (_: C).(\lambda (w: T).(ty3
-g c1 v w))) in (let TMP_145 \def (Bind b) in (let TMP_146 \def (CHead c2
-TMP_145 v) in (let TMP_147 \def (refl_equal C TMP_146) in (let TMP_148 \def
-(ex3_2_intro C T TMP_142 TMP_143 TMP_144 c2 t TMP_147 H13 H11) in (let
-TMP_149 \def (or_introl TMP_128 TMP_137 TMP_148) in (let TMP_150 \def
-(eq_ind_r T v TMP_104 TMP_149 u H7) in (eq_ind_r B b TMP_85 TMP_150 b0
-H8)))))))))))))))))))))))))))))) in (let TMP_152 \def (TMP_151 H6) in
-(TMP_152 H5)))))))))))))))))))))))))))))) in (let TMP_221 \def (\lambda (c0:
-C).(\lambda (c2: C).(\lambda (H1: (wf3 g c0 c2)).(\lambda (H2: (((eq C c0
-(CHead c1 (Bind b) v)) \to (or (ex3_2 C T (\lambda (c3: C).(\lambda (_:
-T).(eq C c2 (CHead c3 (Bind b) v)))) (\lambda (c3: C).(\lambda (_: T).(wf3 g
-c1 c3))) (\lambda (_: C).(\lambda (w: T).(ty3 g c1 v w)))) (ex3 C (\lambda
-(c3: C).(eq C c2 (CHead c3 (Bind Void) (TSort O)))) (\lambda (c3: C).(wf3 g
-c1 c3)) (\lambda (_: C).(\forall (w: T).((ty3 g c1 v w) \to
-False)))))))).(\lambda (u: T).(\lambda (H3: ((\forall (t: T).((ty3 g c0 u t)
-\to False)))).(\lambda (b0: B).(\lambda (H4: (eq C (CHead c0 (Bind b0) u)
-(CHead c1 (Bind b) v))).(let TMP_154 \def (\lambda (e: C).(match e with
-[(CSort _) \Rightarrow c0 | (CHead c _ _) \Rightarrow c])) in (let TMP_155
-\def (Bind b0) in (let TMP_156 \def (CHead c0 TMP_155 u) in (let TMP_157 \def
-(Bind b) in (let TMP_158 \def (CHead c1 TMP_157 v) in (let H5 \def (f_equal C
-C TMP_154 TMP_156 TMP_158 H4) in (let TMP_159 \def (\lambda (e: C).(match e
-with [(CSort _) \Rightarrow b0 | (CHead _ k _) \Rightarrow (match k with
-[(Bind b1) \Rightarrow b1 | (Flat _) \Rightarrow b0])])) in (let TMP_160 \def
-(Bind b0) in (let TMP_161 \def (CHead c0 TMP_160 u) in (let TMP_162 \def
-(Bind b) in (let TMP_163 \def (CHead c1 TMP_162 v) in (let H6 \def (f_equal C
-B TMP_159 TMP_161 TMP_163 H4) in (let TMP_164 \def (\lambda (e: C).(match e
-with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t])) in (let
-TMP_165 \def (Bind b0) in (let TMP_166 \def (CHead c0 TMP_165 u) in (let
-TMP_167 \def (Bind b) in (let TMP_168 \def (CHead c1 TMP_167 v) in (let H7
-\def (f_equal C T TMP_164 TMP_166 TMP_168 H4) in (let TMP_219 \def (\lambda
-(_: (eq B b0 b)).(\lambda (H9: (eq C c0 c1)).(let TMP_169 \def (\lambda (t:
-T).(\forall (t0: T).((ty3 g c0 t t0) \to False))) in (let H10 \def (eq_ind T
-u TMP_169 H3 v H7) in (let TMP_170 \def (\lambda (c: C).(\forall (t: T).((ty3
-g c v t) \to False))) in (let H11 \def (eq_ind C c0 TMP_170 H10 c1 H9) in
-(let TMP_184 \def (\lambda (c: C).((eq C c (CHead c1 (Bind b) v)) \to (let
-TMP_173 \def (\lambda (c3: C).(\lambda (_: T).(let TMP_171 \def (Bind b) in
-(let TMP_172 \def (CHead c3 TMP_171 v) in (eq C c2 TMP_172))))) in (let
-TMP_174 \def (\lambda (c3: C).(\lambda (_: T).(wf3 g c1 c3))) in (let TMP_175
-\def (\lambda (_: C).(\lambda (w: T).(ty3 g c1 v w))) in (let TMP_176 \def
-(ex3_2 C T TMP_173 TMP_174 TMP_175) in (let TMP_180 \def (\lambda (c3:
-C).(let TMP_177 \def (Bind Void) in (let TMP_178 \def (TSort O) in (let
-TMP_179 \def (CHead c3 TMP_177 TMP_178) in (eq C c2 TMP_179))))) in (let
-TMP_181 \def (\lambda (c3: C).(wf3 g c1 c3)) in (let TMP_182 \def (\lambda
-(_: C).(\forall (w: T).((ty3 g c1 v w) \to False))) in (let TMP_183 \def (ex3
-C TMP_180 TMP_181 TMP_182) in (or TMP_176 TMP_183))))))))))) in (let H12 \def
-(eq_ind C c0 TMP_184 H2 c1 H9) in (let TMP_185 \def (\lambda (c: C).(wf3 g c
-c2)) in (let H13 \def (eq_ind C c0 TMP_185 H1 c1 H9) in (let TMP_191 \def
-(\lambda (c3: C).(\lambda (_: T).(let TMP_186 \def (Bind Void) in (let
-TMP_187 \def (TSort O) in (let TMP_188 \def (CHead c2 TMP_186 TMP_187) in
-(let TMP_189 \def (Bind b) in (let TMP_190 \def (CHead c3 TMP_189 v) in (eq C
-TMP_188 TMP_190)))))))) in (let TMP_192 \def (\lambda (c3: C).(\lambda (_:
-T).(wf3 g c1 c3))) in (let TMP_193 \def (\lambda (_: C).(\lambda (w: T).(ty3
-g c1 v w))) in (let TMP_194 \def (ex3_2 C T TMP_191 TMP_192 TMP_193) in (let
-TMP_201 \def (\lambda (c3: C).(let TMP_195 \def (Bind Void) in (let TMP_196
-\def (TSort O) in (let TMP_197 \def (CHead c2 TMP_195 TMP_196) in (let
-TMP_198 \def (Bind Void) in (let TMP_199 \def (TSort O) in (let TMP_200 \def
-(CHead c3 TMP_198 TMP_199) in (eq C TMP_197 TMP_200)))))))) in (let TMP_202
-\def (\lambda (c3: C).(wf3 g c1 c3)) in (let TMP_203 \def (\lambda (_:
-C).(\forall (w: T).((ty3 g c1 v w) \to False))) in (let TMP_204 \def (ex3 C
-TMP_201 TMP_202 TMP_203) in (let TMP_211 \def (\lambda (c3: C).(let TMP_205
-\def (Bind Void) in (let TMP_206 \def (TSort O) in (let TMP_207 \def (CHead
-c2 TMP_205 TMP_206) in (let TMP_208 \def (Bind Void) in (let TMP_209 \def
-(TSort O) in (let TMP_210 \def (CHead c3 TMP_208 TMP_209) in (eq C TMP_207
-TMP_210)))))))) in (let TMP_212 \def (\lambda (c3: C).(wf3 g c1 c3)) in (let
-TMP_213 \def (\lambda (_: C).(\forall (w: T).((ty3 g c1 v w) \to False))) in
-(let TMP_214 \def (Bind Void) in (let TMP_215 \def (TSort O) in (let TMP_216
-\def (CHead c2 TMP_214 TMP_215) in (let TMP_217 \def (refl_equal C TMP_216)
-in (let TMP_218 \def (ex3_intro C TMP_211 TMP_212 TMP_213 c2 TMP_217 H13 H11)
-in (or_intror TMP_194 TMP_204 TMP_218))))))))))))))))))))))))))) in (let
-TMP_220 \def (TMP_219 H6) in (TMP_220 H5))))))))))))))))))))))))))))) in (let
-TMP_241 \def (\lambda (c0: C).(\lambda (c2: C).(\lambda (_: (wf3 g c0
-c2)).(\lambda (_: (((eq C c0 (CHead c1 (Bind b) v)) \to (or (ex3_2 C T
-(\lambda (c3: C).(\lambda (_: T).(eq C c2 (CHead c3 (Bind b) v)))) (\lambda
-(c3: C).(\lambda (_: T).(wf3 g c1 c3))) (\lambda (_: C).(\lambda (w: T).(ty3
-g c1 v w)))) (ex3 C (\lambda (c3: C).(eq C c2 (CHead c3 (Bind Void) (TSort