-u2 H25)) in ((let H27 \def (f_equal C B (\lambda (e: C).(match e in C return
-(\lambda (_: C).B) with [(CSort _) \Rightarrow Abbr | (CHead _ k0 _)
-\Rightarrow (match k0 in K return (\lambda (_: K).B) with [(Bind b0)
-\Rightarrow b0 | (Flat _) \Rightarrow Abbr])])) (CHead d0 (Bind Abbr) u0)
-(CHead c (Bind b) u2) (clear_gen_bind b c (CHead d0 (Bind Abbr) u0) u2 H25))
-in ((let H28 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda
-(_: C).T) with [(CSort _) \Rightarrow u0 | (CHead _ _ t7) \Rightarrow t7]))
-(CHead d0 (Bind Abbr) u0) (CHead c (Bind b) u2) (clear_gen_bind b c (CHead d0
-(Bind Abbr) u0) u2 H25)) in (\lambda (H29: (eq B Abbr b)).(\lambda (_: (eq C
-d0 c)).(let H31 \def (eq_ind T u0 (\lambda (t7: T).(subst0 O t7 t5 t3)) H24
-u2 H28) in (eq_ind B Abbr (\lambda (b0: B).(pc3 (CHead c (Bind b0) u1) t0
-t3)) (ex2_ind T (\lambda (t7: T).(subst0 O t2 t5 t7)) (\lambda (t7: T).(pr0
-t3 t7)) (pc3 (CHead c (Bind Abbr) u1) t0 t3) (\lambda (x: T).(\lambda (H32:
-(subst0 O t2 t5 x)).(\lambda (H33: (pr0 t3 x)).(ex2_ind T (\lambda (t7:
-T).(subst0 O u1 t5 t7)) (\lambda (t7: T).(subst0 (S (plus i O)) u x t7)) (pc3
-(CHead c (Bind Abbr) u1) t0 t3) (\lambda (x0: T).(\lambda (H34: (subst0 O u1
-t5 x0)).(\lambda (H35: (subst0 (S (plus i O)) u x x0)).(let H36 \def (f_equal
+u2 H25)) in (\lambda (H29: (eq B Abbr b)).(\lambda (_: (eq C d0 c)).(let H31
+\def (eq_ind T u0 (\lambda (t7: T).(subst0 O t7 t5 t3)) H24 u2 H28) in
+(eq_ind B Abbr (\lambda (b0: B).(pc3 (CHead c (Bind b0) u1) t0 t3)) (ex2_ind
+T (\lambda (t7: T).(subst0 O t2 t5 t7)) (\lambda (t7: T).(pr0 t3 t7)) (pc3
+(CHead c (Bind Abbr) u1) t0 t3) (\lambda (x: T).(\lambda (H32: (subst0 O t2
+t5 x)).(\lambda (H33: (pr0 t3 x)).(ex2_ind T (\lambda (t7: T).(subst0 O u1 t5
+t7)) (\lambda (t7: T).(subst0 (S (plus i O)) u x t7)) (pc3 (CHead c (Bind
+Abbr) u1) t0 t3) (\lambda (x0: T).(\lambda (H34: (subst0 O u1 t5
+x0)).(\lambda (H35: (subst0 (S (plus i O)) u x x0)).(let H36 \def (f_equal