-x3) H10) in ((let H15 \def (f_equal C B (\lambda (e0: C).(match e0 in C
-return (\lambda (_: C).B) with [(CSort _) \Rightarrow Abbr | (CHead _ k _)
-\Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b)
-\Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr) u) (CHead
-x1 (Bind x0) x3) H10) in ((let H16 \def (f_equal C T (\lambda (e0: C).(match
-e0 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _
-t6) \Rightarrow t6])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H10) in
+x3) H10) in ((let H14 \def (f_equal C B (\lambda (e0: C).(match e0 with
+[(CSort _) \Rightarrow Abbr | (CHead _ k _) \Rightarrow (match k with [(Bind
+b) \Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr) u)
+(CHead x1 (Bind x0) x3) H10) in ((let H15 \def (f_equal C T (\lambda (e0:
+C).(match e0 with [(CSort _) \Rightarrow u | (CHead _ _ t6) \Rightarrow t6]))
+(CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H10) in (\lambda (H16: (eq B
+Abbr x0)).(\lambda (H17: (eq C d x1)).(let H18 \def (eq_ind_r T x3 (\lambda
+(t6: T).(getl i c0 (CHead x2 (Bind x0) t6))) H11 u H15) in (let H19 \def
+(eq_ind_r C x1 (\lambda (c3: C).(csubst0 (minus i0 (S i)) u0 c3 x2)) H12 d
+H17) in (let H20 \def (eq_ind_r B x0 (\lambda (b: B).(getl i c0 (CHead x2
+(Bind b) u))) H18 Abbr H16) in (pc3_pr2_u c0 t0 t2 (pr2_delta c0 x2 u i H20
+t2 t3 H1 t0 H2) t5 (pc3_pr2_r c0 t0 t5 (pr2_delta c0 e u0 i0 (csubst0_getl_ge
+i0 i0 (le_n i0) c c0 u0 H5 (CHead e (Bind Abbr) u0) H6) t0 t0 (pr0_refl t0)
+t5 H4))))))))) H14)) H13))))))))) H9)) (\lambda (H9: (ex4_5 B C C T T
+(\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(\lambda
+(_: T).(eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1))))))) (\lambda
+(b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(getl
+i c0 (CHead e2 (Bind b) w))))))) (\lambda (_: B).(\lambda (_: C).(\lambda (_:
+C).(\lambda (u1: T).(\lambda (w: T).(subst0 (minus i0 (S i)) u0 u1 w))))))
+(\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
+(_: T).(csubst0 (minus i0 (S i)) u0 e1 e2)))))))).(ex4_5_ind B C C T T
+(\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(\lambda
+(_: T).(eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1))))))) (\lambda
+(b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(getl
+i c0 (CHead e2 (Bind b) w))))))) (\lambda (_: B).(\lambda (_: C).(\lambda (_:
+C).(\lambda (u1: T).(\lambda (w: T).(subst0 (minus i0 (S i)) u0 u1 w))))))
+(\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
+(_: T).(csubst0 (minus i0 (S i)) u0 e1 e2)))))) (pc3 c0 t2 t5) (\lambda (x0:
+B).(\lambda (x1: C).(\lambda (x2: C).(\lambda (x3: T).(\lambda (x4:
+T).(\lambda (H10: (eq C (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
+x3))).(\lambda (H11: (getl i c0 (CHead x2 (Bind x0) x4))).(\lambda (H12:
+(subst0 (minus i0 (S i)) u0 x3 x4)).(\lambda (H13: (csubst0 (minus i0 (S i))
+u0 x1 x2)).(let H14 \def (f_equal C C (\lambda (e0: C).(match e0 with [(CSort
+_) \Rightarrow d | (CHead c3 _ _) \Rightarrow c3])) (CHead d (Bind Abbr) u)
+(CHead x1 (Bind x0) x3) H10) in ((let H15 \def (f_equal C B (\lambda (e0:
+C).(match e0 with [(CSort _) \Rightarrow Abbr | (CHead _ k _) \Rightarrow
+(match k with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow Abbr])])) (CHead
+d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H10) in ((let H16 \def (f_equal C T
+(\lambda (e0: C).(match e0 with [(CSort _) \Rightarrow u | (CHead _ _ t6)
+\Rightarrow t6])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3) H10) in