-(CHead c k u2) t1 t2)).(let H1 \def (match H0 in pr2 return (\lambda (c0:
-C).(\lambda (t: T).(\lambda (t0: T).(\lambda (_: (pr2 c0 t t0)).((eq C c0
-(CHead c k u2)) \to ((eq T t t1) \to ((eq T t0 t2) \to (pc3 (CHead c k u1) t1
-t2)))))))) with [(pr2_free c0 t0 t3 H1) \Rightarrow (\lambda (H2: (eq C c0
-(CHead c k u2))).(\lambda (H3: (eq T t0 t1)).(\lambda (H4: (eq T t3
-t2)).(eq_ind C (CHead c k u2) (\lambda (_: C).((eq T t0 t1) \to ((eq T t3 t2)
-\to ((pr0 t0 t3) \to (pc3 (CHead c k u1) t1 t2))))) (\lambda (H5: (eq T t0
-t1)).(eq_ind T t1 (\lambda (t: T).((eq T t3 t2) \to ((pr0 t t3) \to (pc3
-(CHead c k u1) t1 t2)))) (\lambda (H6: (eq T t3 t2)).(eq_ind T t2 (\lambda
-(t: T).((pr0 t1 t) \to (pc3 (CHead c k u1) t1 t2))) (\lambda (H7: (pr0 t1
-t2)).(pc3_pr2_r (CHead c k u1) t1 t2 (pr2_free (CHead c k u1) t1 t2 H7))) t3
-(sym_eq T t3 t2 H6))) t0 (sym_eq T t0 t1 H5))) c0 (sym_eq C c0 (CHead c k u2)
-H2) H3 H4 H1)))) | (pr2_delta c0 d u i H1 t0 t3 H2 t H3) \Rightarrow (\lambda
-(H4: (eq C c0 (CHead c k u2))).(\lambda (H5: (eq T t0 t1)).(\lambda (H6: (eq
-T t t2)).(eq_ind C (CHead c k u2) (\lambda (c1: C).((eq T t0 t1) \to ((eq T t
-t2) \to ((getl i c1 (CHead d (Bind Abbr) u)) \to ((pr0 t0 t3) \to ((subst0 i
-u t3 t) \to (pc3 (CHead c k u1) t1 t2))))))) (\lambda (H7: (eq T t0
-t1)).(eq_ind T t1 (\lambda (t4: T).((eq T t t2) \to ((getl i (CHead c k u2)
-(CHead d (Bind Abbr) u)) \to ((pr0 t4 t3) \to ((subst0 i u t3 t) \to (pc3
-(CHead c k u1) t1 t2)))))) (\lambda (H8: (eq T t t2)).(eq_ind T t2 (\lambda
-(t4: T).((getl i (CHead c k u2) (CHead d (Bind Abbr) u)) \to ((pr0 t1 t3) \to
-((subst0 i u t3 t4) \to (pc3 (CHead c k u1) t1 t2))))) (\lambda (H9: (getl i
-(CHead c k u2) (CHead d (Bind Abbr) u))).(\lambda (H10: (pr0 t1 t3)).(\lambda
-(H11: (subst0 i u t3 t2)).(nat_ind (\lambda (n: nat).((getl n (CHead c k u2)
-(CHead d (Bind Abbr) u)) \to ((subst0 n u t3 t2) \to (pc3 (CHead c k u1) t1
-t2)))) (\lambda (H12: (getl O (CHead c k u2) (CHead d (Bind Abbr)
-u))).(\lambda (H13: (subst0 O u t3 t2)).(K_ind (\lambda (k0: K).((clear
-(CHead c k0 u2) (CHead d (Bind Abbr) u)) \to (pc3 (CHead c k0 u1) t1 t2)))
-(\lambda (b: B).(\lambda (H14: (clear (CHead c (Bind b) u2) (CHead d (Bind
-Abbr) u))).(let H15 \def (f_equal C C (\lambda (e: C).(match e in C return
-(\lambda (_: C).C) with [(CSort _) \Rightarrow d | (CHead c1 _ _) \Rightarrow
-c1])) (CHead d (Bind Abbr) u) (CHead c (Bind b) u2) (clear_gen_bind b c
-(CHead d (Bind Abbr) u) u2 H14)) in ((let H16 \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 d (Bind
-Abbr) u) (CHead c (Bind b) u2) (clear_gen_bind b c (CHead d (Bind Abbr) u) u2
-H14)) in ((let H17 \def (f_equal C T (\lambda (e: C).(match e in C return
-(\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t4) \Rightarrow
-t4])) (CHead d (Bind Abbr) u) (CHead c (Bind b) u2) (clear_gen_bind b c
-(CHead d (Bind Abbr) u) u2 H14)) in (\lambda (H18: (eq B Abbr b)).(\lambda
-(_: (eq C d c)).(let H20 \def (eq_ind T u (\lambda (t4: T).(subst0 O t4 t3
-t2)) H13 u2 H17) in (eq_ind B Abbr (\lambda (b0: B).(pc3 (CHead c (Bind b0)
-u1) t1 t2)) (ex2_ind T (\lambda (t4: T).(subst0 O u1 t3 t4)) (\lambda (t4:
-T).(pr0 t2 t4)) (pc3 (CHead c (Bind Abbr) u1) t1 t2) (\lambda (x: T).(\lambda
-(H21: (subst0 O u1 t3 x)).(\lambda (H22: (pr0 t2 x)).(pc3_pr3_t (CHead c
-(Bind Abbr) u1) t1 x (pr3_pr2 (CHead c (Bind Abbr) u1) t1 x (pr2_delta (CHead
-c (Bind Abbr) u1) c u1 O (getl_refl Abbr c u1) t1 t3 H10 x H21)) t2 (pr3_pr2
-(CHead c (Bind Abbr) u1) t2 x (pr2_free (CHead c (Bind Abbr) u1) t2 x
-H22)))))) (pr0_subst0_fwd u2 t3 t2 O H20 u1 H)) b H18))))) H16)) H15))))
-(\lambda (f: F).(\lambda (H14: (clear (CHead c (Flat f) u2) (CHead d (Bind
-Abbr) u))).(clear_pc3_trans (CHead d (Bind Abbr) u) t1 t2 (pc3_pr2_r (CHead d
-(Bind Abbr) u) t1 t2 (pr2_delta (CHead d (Bind Abbr) u) d u O (getl_refl Abbr
-d u) t1 t3 H10 t2 H13)) (CHead c (Flat f) u1) (clear_flat c (CHead d (Bind
-Abbr) u) (clear_gen_flat f c (CHead d (Bind Abbr) u) u2 H14) f u1)))) k
-(getl_gen_O (CHead c k u2) (CHead d (Bind Abbr) u) H12)))) (\lambda (i0:
-nat).(\lambda (IHi: (((getl i0 (CHead c k u2) (CHead d (Bind Abbr) u)) \to
-((subst0 i0 u t3 t2) \to (pc3 (CHead c k u1) t1 t2))))).(\lambda (H12: (getl
-(S i0) (CHead c k u2) (CHead d (Bind Abbr) u))).(\lambda (H13: (subst0 (S i0)
-u t3 t2)).(K_ind (\lambda (k0: K).((((getl i0 (CHead c k0 u2) (CHead d (Bind
-Abbr) u)) \to ((subst0 i0 u t3 t2) \to (pc3 (CHead c k0 u1) t1 t2)))) \to
-((getl (r k0 i0) c (CHead d (Bind Abbr) u)) \to (pc3 (CHead c k0 u1) t1
-t2)))) (\lambda (b: B).(\lambda (_: (((getl i0 (CHead c (Bind b) u2) (CHead d
-(Bind Abbr) u)) \to ((subst0 i0 u t3 t2) \to (pc3 (CHead c (Bind b) u1) t1
-t2))))).(\lambda (H14: (getl (r (Bind b) i0) c (CHead d (Bind Abbr)
-u))).(pc3_pr2_r (CHead c (Bind b) u1) t1 t2 (pr2_delta (CHead c (Bind b) u1)
-d u (S i0) (getl_head (Bind b) i0 c (CHead d (Bind Abbr) u) H14 u1) t1 t3 H10
-t2 H13))))) (\lambda (f: F).(\lambda (_: (((getl i0 (CHead c (Flat f) u2)
-(CHead d (Bind Abbr) u)) \to ((subst0 i0 u t3 t2) \to (pc3 (CHead c (Flat f)
-u1) t1 t2))))).(\lambda (H14: (getl (r (Flat f) i0) c (CHead d (Bind Abbr)
-u))).(pc3_pr2_r (CHead c (Flat f) u1) t1 t2 (pr2_cflat c t1 t2 (pr2_delta c d
-u (r (Flat f) i0) H14 t1 t3 H10 t2 H13) f u1))))) k IHi (getl_gen_S k c
-(CHead d (Bind Abbr) u) u2 i0 H12)))))) i H9 H11)))) t (sym_eq T t t2 H8)))
-t0 (sym_eq T t0 t1 H7))) c0 (sym_eq C c0 (CHead c k u2) H4) H5 H6 H1 H2
-H3))))]) in (H1 (refl_equal C (CHead c k u2)) (refl_equal T t1) (refl_equal T
-t2)))))))))).
+(CHead c k u2) t1 t2)).(insert_eq C (CHead c k u2) (\lambda (c0: C).(pr2 c0
+t1 t2)) (\lambda (_: C).(pc3 (CHead c k u1) t1 t2)) (\lambda (y: C).(\lambda
+(H1: (pr2 y t1 t2)).(pr2_ind (\lambda (c0: C).(\lambda (t: T).(\lambda (t0:
+T).((eq C c0 (CHead c k u2)) \to (pc3 (CHead c k u1) t t0))))) (\lambda (c0:
+C).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H2: (pr0 t3 t4)).(\lambda (H3:
+(eq C c0 (CHead c k u2))).(let H4 \def (f_equal C C (\lambda (e: C).e) c0
+(CHead c k u2) H3) in (pc3_pr2_r (CHead c k u1) t3 t4 (pr2_free (CHead c k
+u1) t3 t4 H2)))))))) (\lambda (c0: C).(\lambda (d: C).(\lambda (u:
+T).(\lambda (i: nat).(\lambda (H2: (getl i c0 (CHead d (Bind Abbr)
+u))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H3: (pr0 t3 t4)).(\lambda
+(t: T).(\lambda (H4: (subst0 i u t4 t)).(\lambda (H5: (eq C c0 (CHead c k
+u2))).(let H6 \def (f_equal C C (\lambda (e: C).e) c0 (CHead c k u2) H5) in
+(let H7 \def (eq_ind C c0 (\lambda (c1: C).(getl i c1 (CHead d (Bind Abbr)
+u))) H2 (CHead c k u2) H6) in (nat_ind (\lambda (n: nat).((getl n (CHead c k
+u2) (CHead d (Bind Abbr) u)) \to ((subst0 n u t4 t) \to (pc3 (CHead c k u1)
+t3 t)))) (\lambda (H8: (getl O (CHead c k u2) (CHead d (Bind Abbr)
+u))).(\lambda (H9: (subst0 O u t4 t)).(K_ind (\lambda (k0: K).((clear (CHead
+c k0 u2) (CHead d (Bind Abbr) u)) \to (pc3 (CHead c k0 u1) t3 t))) (\lambda
+(b: B).(\lambda (H10: (clear (CHead c (Bind b) u2) (CHead d (Bind Abbr)
+u))).(let H11 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda
+(_: C).C) with [(CSort _) \Rightarrow d | (CHead c1 _ _) \Rightarrow c1]))
+(CHead d (Bind Abbr) u) (CHead c (Bind b) u2) (clear_gen_bind b c (CHead d
+(Bind Abbr) u) u2 H10)) in ((let H12 \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 d (Bind Abbr) u)
+(CHead c (Bind b) u2) (clear_gen_bind b c (CHead d (Bind Abbr) u) u2 H10)) in
+((let H13 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_:
+C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) (CHead
+d (Bind Abbr) u) (CHead c (Bind b) u2) (clear_gen_bind b c (CHead d (Bind
+Abbr) u) u2 H10)) in (\lambda (H14: (eq B Abbr b)).(\lambda (_: (eq C d
+c)).(let H16 \def (eq_ind T u (\lambda (t0: T).(subst0 O t0 t4 t)) H9 u2 H13)
+in (eq_ind B Abbr (\lambda (b0: B).(pc3 (CHead c (Bind b0) u1) t3 t))
+(ex2_ind T (\lambda (t0: T).(subst0 O u1 t4 t0)) (\lambda (t0: T).(pr0 t t0))
+(pc3 (CHead c (Bind Abbr) u1) t3 t) (\lambda (x: T).(\lambda (H17: (subst0 O
+u1 t4 x)).(\lambda (H18: (pr0 t x)).(pc3_pr3_t (CHead c (Bind Abbr) u1) t3 x
+(pr3_pr2 (CHead c (Bind Abbr) u1) t3 x (pr2_delta (CHead c (Bind Abbr) u1) c
+u1 O (getl_refl Abbr c u1) t3 t4 H3 x H17)) t (pr3_pr2 (CHead c (Bind Abbr)
+u1) t x (pr2_free (CHead c (Bind Abbr) u1) t x H18)))))) (pr0_subst0_fwd u2
+t4 t O H16 u1 H)) b H14))))) H12)) H11)))) (\lambda (f: F).(\lambda (H10:
+(clear (CHead c (Flat f) u2) (CHead d (Bind Abbr) u))).(clear_pc3_trans
+(CHead d (Bind Abbr) u) t3 t (pc3_pr2_r (CHead d (Bind Abbr) u) t3 t
+(pr2_delta (CHead d (Bind Abbr) u) d u O (getl_refl Abbr d u) t3 t4 H3 t H9))
+(CHead c (Flat f) u1) (clear_flat c (CHead d (Bind Abbr) u) (clear_gen_flat f
+c (CHead d (Bind Abbr) u) u2 H10) f u1)))) k (getl_gen_O (CHead c k u2)
+(CHead d (Bind Abbr) u) H8)))) (\lambda (i0: nat).(\lambda (IHi: (((getl i0
+(CHead c k u2) (CHead d (Bind Abbr) u)) \to ((subst0 i0 u t4 t) \to (pc3
+(CHead c k u1) t3 t))))).(\lambda (H8: (getl (S i0) (CHead c k u2) (CHead d
+(Bind Abbr) u))).(\lambda (H9: (subst0 (S i0) u t4 t)).(K_ind (\lambda (k0:
+K).((((getl i0 (CHead c k0 u2) (CHead d (Bind Abbr) u)) \to ((subst0 i0 u t4
+t) \to (pc3 (CHead c k0 u1) t3 t)))) \to ((getl (r k0 i0) c (CHead d (Bind
+Abbr) u)) \to (pc3 (CHead c k0 u1) t3 t)))) (\lambda (b: B).(\lambda (_:
+(((getl i0 (CHead c (Bind b) u2) (CHead d (Bind Abbr) u)) \to ((subst0 i0 u
+t4 t) \to (pc3 (CHead c (Bind b) u1) t3 t))))).(\lambda (H10: (getl (r (Bind
+b) i0) c (CHead d (Bind Abbr) u))).(pc3_pr2_r (CHead c (Bind b) u1) t3 t
+(pr2_delta (CHead c (Bind b) u1) d u (S i0) (getl_head (Bind b) i0 c (CHead d
+(Bind Abbr) u) H10 u1) t3 t4 H3 t H9))))) (\lambda (f: F).(\lambda (_:
+(((getl i0 (CHead c (Flat f) u2) (CHead d (Bind Abbr) u)) \to ((subst0 i0 u
+t4 t) \to (pc3 (CHead c (Flat f) u1) t3 t))))).(\lambda (H10: (getl (r (Flat
+f) i0) c (CHead d (Bind Abbr) u))).(pc3_pr2_r (CHead c (Flat f) u1) t3 t
+(pr2_cflat c t3 t (pr2_delta c d u (r (Flat f) i0) H10 t3 t4 H3 t H9) f
+u1))))) k IHi (getl_gen_S k c (CHead d (Bind Abbr) u) u2 i0 H8)))))) i H7
+H4)))))))))))))) y t1 t2 H1))) H0)))))))).