-(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 (pr3 (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 (pr3 (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 (pr3
-(CHead c k u1) t1 t2)))) (\lambda (H6: (eq T t3 t2)).(eq_ind T t2 (\lambda
-(t: T).((pr0 t1 t) \to (pr3 (CHead c k u1) t1 t2))) (\lambda (H7: (pr0 t1
-t2)).(pr3_pr2 (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 (pr3 (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 (pr3
-(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 (pr3 (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 (pr3 (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).((getl O
-(CHead c k0 u2) (CHead d (Bind Abbr) u)) \to (pr3 (CHead c k0 u1) t1 t2)))
-(\lambda (b: B).(\lambda (H14: (getl O (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 (getl_gen_O (CHead c (Bind b) u2) (CHead d (Bind
-Abbr) u) 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
-(getl_gen_O (CHead c (Bind b) u2) (CHead d (Bind Abbr) u) 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 (getl_gen_O (CHead c (Bind b) u2) (CHead d (Bind Abbr) u) 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).(pr3 (CHead c (Bind b0) u1) t1 t2)) (ex2_ind T (\lambda (t4:
-T).(subst0 O u1 t3 t4)) (\lambda (t4: T).(pr0 t4 t2)) (pr3 (CHead c (Bind
-Abbr) u1) t1 t2) (\lambda (x: T).(\lambda (H21: (subst0 O u1 t3 x)).(\lambda
-(H22: (pr0 x t2)).(pr3_sing (CHead c (Bind Abbr) u1) x t1 (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) x t2 (pr2_free (CHead c (Bind Abbr) u1) x t2
-H22)))))) (pr0_subst0_back u2 t3 t2 O H20 u1 H)) b H18))))) H16)) H15))))
-(\lambda (f: F).(\lambda (H14: (getl O (CHead c (Flat f) u2) (CHead d (Bind
-Abbr) u))).(pr3_pr2 (CHead c (Flat f) u1) t1 t2 (pr2_cflat c t1 t2 (pr2_delta
-c d u O (getl_intro O c (CHead d (Bind Abbr) u) c (drop_refl c)
-(clear_gen_flat f c (CHead d (Bind Abbr) u) u2 (getl_gen_O (CHead c (Flat f)
-u2) (CHead d (Bind Abbr) u) H14))) t1 t3 H10 t2 H13) f u1)))) k H12)))
-(\lambda (i0: nat).(\lambda (IHi: (((getl i0 (CHead c k u2) (CHead d (Bind
-Abbr) u)) \to ((subst0 i0 u t3 t2) \to (pr3 (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
-(S i0) (CHead c k0 u2) (CHead d (Bind Abbr) u)) \to ((((getl i0 (CHead c k0
-u2) (CHead d (Bind Abbr) u)) \to ((subst0 i0 u t3 t2) \to (pr3 (CHead c k0
-u1) t1 t2)))) \to (pr3 (CHead c k0 u1) t1 t2)))) (\lambda (b: B).(\lambda
-(H14: (getl (S i0) (CHead c (Bind b) u2) (CHead d (Bind Abbr) u))).(\lambda
-(_: (((getl i0 (CHead c (Bind b) u2) (CHead d (Bind Abbr) u)) \to ((subst0 i0
-u t3 t2) \to (pr3 (CHead c (Bind b) u1) t1 t2))))).(pr3_pr2 (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) (getl_gen_S (Bind b) c (CHead d (Bind Abbr) u) u2
-i0 H14) u1) t1 t3 H10 t2 H13))))) (\lambda (f: F).(\lambda (H14: (getl (S i0)
-(CHead c (Flat f) u2) (CHead d (Bind Abbr) u))).(\lambda (_: (((getl i0
-(CHead c (Flat f) u2) (CHead d (Bind Abbr) u)) \to ((subst0 i0 u t3 t2) \to
-(pr3 (CHead c (Flat f) u1) t1 t2))))).(pr3_pr2 (CHead c (Flat f) u1) t1 t2
-(pr2_cflat c t1 t2 (pr2_delta c d u (r (Flat f) i0) (getl_gen_S (Flat f) c
-(CHead d (Bind Abbr) u) u2 i0 H14) t1 t3 H10 t2 H13) f u1))))) k H12 IHi)))))
-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).(pr3 (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 (pr3 (CHead c k u1) t t0))))) (\lambda (c0:
+C).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H2: (pr0 t3 t4)).(\lambda (_:
+(eq C c0 (CHead c k u2))).(pr3_pr2 (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
+(eq_ind C c0 (\lambda (c1: C).(getl i c1 (CHead d (Bind Abbr) u))) H2 (CHead
+c k u2) H5) in (nat_ind (\lambda (n: nat).((getl n (CHead c k u2) (CHead d
+(Bind Abbr) u)) \to ((subst0 n u t4 t) \to (pr3 (CHead c k u1) t3 t))))
+(\lambda (H7: (getl O (CHead c k u2) (CHead d (Bind Abbr) u))).(\lambda (H8:
+(subst0 O u t4 t)).(K_ind (\lambda (k0: K).((getl O (CHead c k0 u2) (CHead d
+(Bind Abbr) u)) \to (pr3 (CHead c k0 u1) t3 t))) (\lambda (b: B).(\lambda
+(H9: (getl O (CHead c (Bind b) u2) (CHead d (Bind Abbr) u))).(let H10 \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
+(getl_gen_O (CHead c (Bind b) u2) (CHead d (Bind Abbr) u) H9))) in ((let H11
+\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 (getl_gen_O (CHead c (Bind b)
+u2) (CHead d (Bind Abbr) u) H9))) in ((let H12 \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 (getl_gen_O (CHead c (Bind
+b) u2) (CHead d (Bind Abbr) u) H9))) in (\lambda (H13: (eq B Abbr
+b)).(\lambda (_: (eq C d c)).(let H15 \def (eq_ind T u (\lambda (t0:
+T).(subst0 O t0 t4 t)) H8 u2 H12) in (eq_ind B Abbr (\lambda (b0: B).(pr3
+(CHead c (Bind b0) u1) t3 t)) (ex2_ind T (\lambda (t0: T).(subst0 O u1 t4
+t0)) (\lambda (t0: T).(pr0 t0 t)) (pr3 (CHead c (Bind Abbr) u1) t3 t)
+(\lambda (x: T).(\lambda (H16: (subst0 O u1 t4 x)).(\lambda (H17: (pr0 x
+t)).(pr3_sing (CHead c (Bind Abbr) u1) x t3 (pr2_delta (CHead c (Bind Abbr)
+u1) c u1 O (getl_refl Abbr c u1) t3 t4 H3 x H16) t (pr3_pr2 (CHead c (Bind
+Abbr) u1) x t (pr2_free (CHead c (Bind Abbr) u1) x t H17))))))
+(pr0_subst0_back u2 t4 t O H15 u1 H)) b H13))))) H11)) H10)))) (\lambda (f:
+F).(\lambda (H9: (getl O (CHead c (Flat f) u2) (CHead d (Bind Abbr)
+u))).(pr3_pr2 (CHead c (Flat f) u1) t3 t (pr2_cflat c t3 t (pr2_delta c d u O
+(getl_intro O c (CHead d (Bind Abbr) u) c (drop_refl c) (clear_gen_flat f c
+(CHead d (Bind Abbr) u) u2 (getl_gen_O (CHead c (Flat f) u2) (CHead d (Bind
+Abbr) u) H9))) t3 t4 H3 t H8) f u1)))) k H7))) (\lambda (i0: nat).(\lambda
+(IHi: (((getl i0 (CHead c k u2) (CHead d (Bind Abbr) u)) \to ((subst0 i0 u t4
+t) \to (pr3 (CHead c k u1) t3 t))))).(\lambda (H7: (getl (S i0) (CHead c k
+u2) (CHead d (Bind Abbr) u))).(\lambda (H8: (subst0 (S i0) u t4 t)).(K_ind
+(\lambda (k0: K).((getl (S i0) (CHead c k0 u2) (CHead d (Bind Abbr) u)) \to
+((((getl i0 (CHead c k0 u2) (CHead d (Bind Abbr) u)) \to ((subst0 i0 u t4 t)
+\to (pr3 (CHead c k0 u1) t3 t)))) \to (pr3 (CHead c k0 u1) t3 t)))) (\lambda
+(b: B).(\lambda (H9: (getl (S i0) (CHead c (Bind b) u2) (CHead d (Bind Abbr)
+u))).(\lambda (_: (((getl i0 (CHead c (Bind b) u2) (CHead d (Bind Abbr) u))
+\to ((subst0 i0 u t4 t) \to (pr3 (CHead c (Bind b) u1) t3 t))))).(pr3_pr2
+(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) (getl_gen_S (Bind b) c
+(CHead d (Bind Abbr) u) u2 i0 H9) u1) t3 t4 H3 t H8))))) (\lambda (f:
+F).(\lambda (H9: (getl (S i0) (CHead c (Flat f) u2) (CHead d (Bind Abbr)
+u))).(\lambda (_: (((getl i0 (CHead c (Flat f) u2) (CHead d (Bind Abbr) u))
+\to ((subst0 i0 u t4 t) \to (pr3 (CHead c (Flat f) u1) t3 t))))).(pr3_pr2
+(CHead c (Flat f) u1) t3 t (pr2_cflat c t3 t (pr2_delta c d u (r (Flat f) i0)
+(getl_gen_S (Flat f) c (CHead d (Bind Abbr) u) u2 i0 H9) t3 t4 H3 t H8) f
+u1))))) k H7 IHi))))) i H6 H4))))))))))))) y t1 t2 H1))) H0)))))))).