-(\lambda (u2: T).(eq T t6 (THead (Bind b) u2 t2))) (\lambda (u2: T).(subst0 i
-u0 u u2)) (ty3 g c t6 (THead (Bind b) u t3)) (\lambda (x: T).(\lambda (H10:
-(eq T t6 (THead (Bind b) x t2))).(\lambda (H11: (subst0 i u0 u x)).(eq_ind_r
-T (THead (Bind b) x t2) (\lambda (t7: T).(ty3 g c t7 (THead (Bind b) u t3)))
-(ex_ind T (\lambda (t7: T).(ty3 g (CHead c (Bind b) u) t4 t7)) (ty3 g c
-(THead (Bind b) x t2) (THead (Bind b) u t3)) (\lambda (x0: T).(\lambda (H12:
-(ty3 g (CHead c (Bind b) u) t4 x0)).(ex_ind T (\lambda (t7: T).(ty3 g (CHead
-c (Bind b) x) t3 t7)) (ty3 g c (THead (Bind b) x t2) (THead (Bind b) u t3))
-(\lambda (x1: T).(\lambda (H13: (ty3 g (CHead c (Bind b) x) t3 x1)).(ty3_conv
-g c (THead (Bind b) u t3) (THead (Bind b) u t4) (ty3_bind g c u t0 H0 b t3 t4
-H4 x0 H12) (THead (Bind b) x t2) (THead (Bind b) x t3) (ty3_bind g c x t0 (H1
-i u0 c x (fsubst0_snd i u0 c u x H11) e H8) b t2 t3 (H3 (S i) u0 (CHead c
-(Bind b) x) t2 (fsubst0_fst (S i) u0 (CHead c (Bind b) u) t2 (CHead c (Bind
-b) x) (csubst0_snd_bind b i u0 u x H11 c)) e (getl_head (Bind b) i c (CHead e
-(Bind Abbr) u0) H8 u)) x1 H13) (pc3_fsubst0 c (THead (Bind b) u t3) (THead
-(Bind b) u t3) (pc3_refl c (THead (Bind b) u t3)) i u0 c (THead (Bind b) x
-t3) (fsubst0_snd i u0 c (THead (Bind b) u t3) (THead (Bind b) x t3)
-(subst0_fst u0 x u i H11 t3 (Bind b))) e H8)))) (ty3_correct g (CHead c (Bind
-b) x) t2 t3 (H3 (S i) u0 (CHead c (Bind b) x) t2 (fsubst0_fst (S i) u0 (CHead
-c (Bind b) u) t2 (CHead c (Bind b) x) (csubst0_snd_bind b i u0 u x H11 c)) e
-(getl_head (Bind b) i c (CHead e (Bind Abbr) u0) H8 u)))))) (ty3_correct g
-(CHead c (Bind b) u) t3 t4 H4)) t6 H10)))) H9)) (\lambda (H9: (ex2 T (\lambda
-(t7: T).(eq T t6 (THead (Bind b) u t7))) (\lambda (t7: T).(subst0 (s (Bind b)
-i) u0 t2 t7)))).(ex2_ind T (\lambda (t7: T).(eq T t6 (THead (Bind b) u t7)))
-(\lambda (t7: T).(subst0 (s (Bind b) i) u0 t2 t7)) (ty3 g c t6 (THead (Bind
-b) u t3)) (\lambda (x: T).(\lambda (H10: (eq T t6 (THead (Bind b) u
-x))).(\lambda (H11: (subst0 (s (Bind b) i) u0 t2 x)).(eq_ind_r T (THead (Bind
-b) u x) (\lambda (t7: T).(ty3 g c t7 (THead (Bind b) u t3))) (ex_ind T
-(\lambda (t7: T).(ty3 g (CHead c (Bind b) u) t3 t7)) (ty3 g c (THead (Bind b)
-u x) (THead (Bind b) u t3)) (\lambda (x0: T).(\lambda (H12: (ty3 g (CHead c
-(Bind b) u) t3 x0)).(ty3_bind g c u t0 H0 b x t3 (H3 (S i) u0 (CHead c (Bind
-b) u) x (fsubst0_snd (S i) u0 (CHead c (Bind b) u) t2 x H11) e (getl_head
-(Bind b) i c (CHead e (Bind Abbr) u0) H8 u)) x0 H12))) (ty3_correct g (CHead
-c (Bind b) u) x t3 (H3 (S i) u0 (CHead c (Bind b) u) x (fsubst0_snd (S i) u0
-(CHead c (Bind b) u) t2 x H11) e (getl_head (Bind b) i c (CHead e (Bind Abbr)
-u0) H8 u)))) t6 H10)))) H9)) (\lambda (H9: (ex3_2 T T (\lambda (u2:
-T).(\lambda (t7: T).(eq T t6 (THead (Bind b) u2 t7)))) (\lambda (u2:
-T).(\lambda (_: T).(subst0 i u0 u u2))) (\lambda (_: T).(\lambda (t7:
-T).(subst0 (s (Bind b) i) u0 t2 t7))))).(ex3_2_ind T T (\lambda (u2:
-T).(\lambda (t7: T).(eq T t6 (THead (Bind b) u2 t7)))) (\lambda (u2:
-T).(\lambda (_: T).(subst0 i u0 u u2))) (\lambda (_: T).(\lambda (t7:
-T).(subst0 (s (Bind b) i) u0 t2 t7))) (ty3 g c t6 (THead (Bind b) u t3))
-(\lambda (x0: T).(\lambda (x1: T).(\lambda (H10: (eq T t6 (THead (Bind b) x0
-x1))).(\lambda (H11: (subst0 i u0 u x0)).(\lambda (H12: (subst0 (s (Bind b)
-i) u0 t2 x1)).(eq_ind_r T (THead (Bind b) x0 x1) (\lambda (t7: T).(ty3 g c t7
-(THead (Bind b) u t3))) (ex_ind T (\lambda (t7: T).(ty3 g (CHead c (Bind b)
-u) t4 t7)) (ty3 g c (THead (Bind b) x0 x1) (THead (Bind b) u t3)) (\lambda
-(x: T).(\lambda (H13: (ty3 g (CHead c (Bind b) u) t4 x)).(ex_ind T (\lambda
-(t7: T).(ty3 g (CHead c (Bind b) x0) t3 t7)) (ty3 g c (THead (Bind b) x0 x1)
-(THead (Bind b) u t3)) (\lambda (x2: T).(\lambda (H14: (ty3 g (CHead c (Bind
-b) x0) t3 x2)).(ty3_conv g c (THead (Bind b) u t3) (THead (Bind b) u t4)
-(ty3_bind g c u t0 H0 b t3 t4 H4 x H13) (THead (Bind b) x0 x1) (THead (Bind
-b) x0 t3) (ty3_bind g c x0 t0 (H1 i u0 c x0 (fsubst0_snd i u0 c u x0 H11) e
-H8) b x1 t3 (H3 (S i) u0 (CHead c (Bind b) x0) x1 (fsubst0_both (S i) u0
-(CHead c (Bind b) u) t2 x1 H12 (CHead c (Bind b) x0) (csubst0_snd_bind b i u0
-u x0 H11 c)) e (getl_head (Bind b) i c (CHead e (Bind Abbr) u0) H8 u)) x2
-H14) (pc3_fsubst0 c (THead (Bind b) u t3) (THead (Bind b) u t3) (pc3_refl c
-(THead (Bind b) u t3)) i u0 c (THead (Bind b) x0 t3) (fsubst0_snd i u0 c
-(THead (Bind b) u t3) (THead (Bind b) x0 t3) (subst0_fst u0 x0 u i H11 t3
-(Bind b))) e H8)))) (ty3_correct g (CHead c (Bind b) x0) x1 t3 (H3 (S i) u0
-(CHead c (Bind b) x0) x1 (fsubst0_both (S i) u0 (CHead c (Bind b) u) t2 x1
-H12 (CHead c (Bind b) x0) (csubst0_snd_bind b i u0 u x0 H11 c)) e (getl_head
-(Bind b) i c (CHead e (Bind Abbr) u0) H8 u)))))) (ty3_correct g (CHead c
-(Bind b) u) t3 t4 H4)) t6 H10)))))) H9)) (subst0_gen_head (Bind b) u0 u t2 t6
-i H7)))))) (\lambda (c3: C).(\lambda (H7: (csubst0 i u0 c c3)).(\lambda (e:
-C).(\lambda (H8: (getl i c (CHead e (Bind Abbr) u0))).(ex_ind T (\lambda (t6:
-T).(ty3 g (CHead c3 (Bind b) u) t3 t6)) (ty3 g c3 (THead (Bind b) u t2)
-(THead (Bind b) u t3)) (\lambda (x: T).(\lambda (H9: (ty3 g (CHead c3 (Bind
-b) u) t3 x)).(ty3_bind g c3 u t0 (H1 i u0 c3 u (fsubst0_fst i u0 c u c3 H7) e
-H8) b t2 t3 (H3 (S i) u0 (CHead c3 (Bind b) u) t2 (fsubst0_fst (S i) u0
-(CHead c (Bind b) u) t2 (CHead c3 (Bind b) u) (csubst0_fst_bind b i c c3 u0
-H7 u)) e (getl_head (Bind b) i c (CHead e (Bind Abbr) u0) H8 u)) x H9)))
-(ty3_correct g (CHead c3 (Bind b) u) t2 t3 (H3 (S i) u0 (CHead c3 (Bind b) u)
-t2 (fsubst0_fst (S i) u0 (CHead c (Bind b) u) t2 (CHead c3 (Bind b) u)
-(csubst0_fst_bind b i c c3 u0 H7 u)) e (getl_head (Bind b) i c (CHead e (Bind
-Abbr) u0) H8 u)))))))) (\lambda (t6: T).(\lambda (H7: (subst0 i u0 (THead
-(Bind b) u t2) t6)).(\lambda (c3: C).(\lambda (H8: (csubst0 i u0 c
-c3)).(\lambda (e: C).(\lambda (H9: (getl i c (CHead e (Bind Abbr)
-u0))).(or3_ind (ex2 T (\lambda (u2: T).(eq T t6 (THead (Bind b) u2 t2)))
-(\lambda (u2: T).(subst0 i u0 u u2))) (ex2 T (\lambda (t7: T).(eq T t6 (THead
-(Bind b) u t7))) (\lambda (t7: T).(subst0 (s (Bind b) i) u0 t2 t7))) (ex3_2 T
-T (\lambda (u2: T).(\lambda (t7: T).(eq T t6 (THead (Bind b) u2 t7))))
+(\lambda (u2: T).(eq T t5 (THead (Bind b) u2 t2))) (\lambda (u2: T).(subst0 i
+u0 u u2)) (ty3 g c t5 (THead (Bind b) u t3)) (\lambda (x: T).(\lambda (H8:
+(eq T t5 (THead (Bind b) x t2))).(\lambda (H9: (subst0 i u0 u x)).(eq_ind_r T
+(THead (Bind b) x t2) (\lambda (t6: T).(ty3 g c t6 (THead (Bind b) u t3)))
+(ex_ind T (\lambda (t6: T).(ty3 g (CHead c (Bind b) u) t3 t6)) (ty3 g c
+(THead (Bind b) x t2) (THead (Bind b) u t3)) (\lambda (x0: T).(\lambda (H10:
+(ty3 g (CHead c (Bind b) u) t3 x0)).(ex_ind T (\lambda (t6: T).(ty3 g (CHead
+c (Bind b) x) t3 t6)) (ty3 g c (THead (Bind b) x t2) (THead (Bind b) u t3))
+(\lambda (x1: T).(\lambda (_: (ty3 g (CHead c (Bind b) x) t3 x1)).(ty3_conv g
+c (THead (Bind b) u t3) (THead (Bind b) u x0) (ty3_bind g c u t0 H0 b t3 x0
+H10) (THead (Bind b) x t2) (THead (Bind b) x t3) (ty3_bind g c x t0 (H1 i u0
+c x (fsubst0_snd i u0 c u x H9) e H6) b t2 t3 (H3 (S i) u0 (CHead c (Bind b)
+x) t2 (fsubst0_fst (S i) u0 (CHead c (Bind b) u) t2 (CHead c (Bind b) x)
+(csubst0_snd_bind b i u0 u x H9 c)) e (getl_head (Bind b) i c (CHead e (Bind
+Abbr) u0) H6 u))) (pc3_fsubst0 c (THead (Bind b) u t3) (THead (Bind b) u t3)
+(pc3_refl c (THead (Bind b) u t3)) i u0 c (THead (Bind b) x t3) (fsubst0_snd
+i u0 c (THead (Bind b) u t3) (THead (Bind b) x t3) (subst0_fst u0 x u i H9 t3
+(Bind b))) e H6)))) (ty3_correct g (CHead c (Bind b) x) t2 t3 (H3 (S i) u0
+(CHead c (Bind b) x) t2 (fsubst0_fst (S i) u0 (CHead c (Bind b) u) t2 (CHead
+c (Bind b) x) (csubst0_snd_bind b i u0 u x H9 c)) e (getl_head (Bind b) i c
+(CHead e (Bind Abbr) u0) H6 u)))))) (ty3_correct g (CHead c (Bind b) u) t2 t3
+H2)) t5 H8)))) H7)) (\lambda (H7: (ex2 T (\lambda (t6: T).(eq T t5 (THead
+(Bind b) u t6))) (\lambda (t6: T).(subst0 (s (Bind b) i) u0 t2
+t6)))).(ex2_ind T (\lambda (t6: T).(eq T t5 (THead (Bind b) u t6))) (\lambda
+(t6: T).(subst0 (s (Bind b) i) u0 t2 t6)) (ty3 g c t5 (THead (Bind b) u t3))
+(\lambda (x: T).(\lambda (H8: (eq T t5 (THead (Bind b) u x))).(\lambda (H9:
+(subst0 (s (Bind b) i) u0 t2 x)).(eq_ind_r T (THead (Bind b) u x) (\lambda
+(t6: T).(ty3 g c t6 (THead (Bind b) u t3))) (ex_ind T (\lambda (t6: T).(ty3 g
+(CHead c (Bind b) u) t3 t6)) (ty3 g c (THead (Bind b) u x) (THead (Bind b) u
+t3)) (\lambda (x0: T).(\lambda (_: (ty3 g (CHead c (Bind b) u) t3
+x0)).(ty3_bind g c u t0 H0 b x t3 (H3 (S i) u0 (CHead c (Bind b) u) x
+(fsubst0_snd (S i) u0 (CHead c (Bind b) u) t2 x H9) e (getl_head (Bind b) i c
+(CHead e (Bind Abbr) u0) H6 u))))) (ty3_correct g (CHead c (Bind b) u) x t3
+(H3 (S i) u0 (CHead c (Bind b) u) x (fsubst0_snd (S i) u0 (CHead c (Bind b)
+u) t2 x H9) e (getl_head (Bind b) i c (CHead e (Bind Abbr) u0) H6 u)))) t5
+H8)))) H7)) (\lambda (H7: (ex3_2 T T (\lambda (u2: T).(\lambda (t6: T).(eq T
+t5 (THead (Bind b) u2 t6)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i u0 u
+u2))) (\lambda (_: T).(\lambda (t6: T).(subst0 (s (Bind b) i) u0 t2
+t6))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t6: T).(eq T t5 (THead
+(Bind b) u2 t6)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i u0 u u2)))
+(\lambda (_: T).(\lambda (t6: T).(subst0 (s (Bind b) i) u0 t2 t6))) (ty3 g c
+t5 (THead (Bind b) u t3)) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H8: (eq
+T t5 (THead (Bind b) x0 x1))).(\lambda (H9: (subst0 i u0 u x0)).(\lambda
+(H10: (subst0 (s (Bind b) i) u0 t2 x1)).(eq_ind_r T (THead (Bind b) x0 x1)
+(\lambda (t6: T).(ty3 g c t6 (THead (Bind b) u t3))) (ex_ind T (\lambda (t6:
+T).(ty3 g (CHead c (Bind b) u) t3 t6)) (ty3 g c (THead (Bind b) x0 x1) (THead
+(Bind b) u t3)) (\lambda (x: T).(\lambda (H11: (ty3 g (CHead c (Bind b) u) t3
+x)).(ex_ind T (\lambda (t6: T).(ty3 g (CHead c (Bind b) x0) t3 t6)) (ty3 g c
+(THead (Bind b) x0 x1) (THead (Bind b) u t3)) (\lambda (x2: T).(\lambda (_:
+(ty3 g (CHead c (Bind b) x0) t3 x2)).(ty3_conv g c (THead (Bind b) u t3)
+(THead (Bind b) u x) (ty3_bind g c u t0 H0 b t3 x H11) (THead (Bind b) x0 x1)
+(THead (Bind b) x0 t3) (ty3_bind g c x0 t0 (H1 i u0 c x0 (fsubst0_snd i u0 c
+u x0 H9) e H6) b x1 t3 (H3 (S i) u0 (CHead c (Bind b) x0) x1 (fsubst0_both (S
+i) u0 (CHead c (Bind b) u) t2 x1 H10 (CHead c (Bind b) x0) (csubst0_snd_bind
+b i u0 u x0 H9 c)) e (getl_head (Bind b) i c (CHead e (Bind Abbr) u0) H6 u)))
+(pc3_fsubst0 c (THead (Bind b) u t3) (THead (Bind b) u t3) (pc3_refl c (THead
+(Bind b) u t3)) i u0 c (THead (Bind b) x0 t3) (fsubst0_snd i u0 c (THead
+(Bind b) u t3) (THead (Bind b) x0 t3) (subst0_fst u0 x0 u i H9 t3 (Bind b)))
+e H6)))) (ty3_correct g (CHead c (Bind b) x0) x1 t3 (H3 (S i) u0 (CHead c
+(Bind b) x0) x1 (fsubst0_both (S i) u0 (CHead c (Bind b) u) t2 x1 H10 (CHead
+c (Bind b) x0) (csubst0_snd_bind b i u0 u x0 H9 c)) e (getl_head (Bind b) i c
+(CHead e (Bind Abbr) u0) H6 u)))))) (ty3_correct g (CHead c (Bind b) u) t2 t3
+H2)) t5 H8)))))) H7)) (subst0_gen_head (Bind b) u0 u t2 t5 i H5))))))
+(\lambda (c3: C).(\lambda (H5: (csubst0 i u0 c c3)).(\lambda (e: C).(\lambda
+(H6: (getl i c (CHead e (Bind Abbr) u0))).(ex_ind T (\lambda (t5: T).(ty3 g
+(CHead c3 (Bind b) u) t3 t5)) (ty3 g c3 (THead (Bind b) u t2) (THead (Bind b)
+u t3)) (\lambda (x: T).(\lambda (_: (ty3 g (CHead c3 (Bind b) u) t3
+x)).(ty3_bind g c3 u t0 (H1 i u0 c3 u (fsubst0_fst i u0 c u c3 H5) e H6) b t2
+t3 (H3 (S i) u0 (CHead c3 (Bind b) u) t2 (fsubst0_fst (S i) u0 (CHead c (Bind
+b) u) t2 (CHead c3 (Bind b) u) (csubst0_fst_bind b i c c3 u0 H5 u)) e
+(getl_head (Bind b) i c (CHead e (Bind Abbr) u0) H6 u))))) (ty3_correct g
+(CHead c3 (Bind b) u) t2 t3 (H3 (S i) u0 (CHead c3 (Bind b) u) t2
+(fsubst0_fst (S i) u0 (CHead c (Bind b) u) t2 (CHead c3 (Bind b) u)
+(csubst0_fst_bind b i c c3 u0 H5 u)) e (getl_head (Bind b) i c (CHead e (Bind
+Abbr) u0) H6 u)))))))) (\lambda (t5: T).(\lambda (H5: (subst0 i u0 (THead
+(Bind b) u t2) t5)).(\lambda (c3: C).(\lambda (H6: (csubst0 i u0 c
+c3)).(\lambda (e: C).(\lambda (H7: (getl i c (CHead e (Bind Abbr)
+u0))).(or3_ind (ex2 T (\lambda (u2: T).(eq T t5 (THead (Bind b) u2 t2)))
+(\lambda (u2: T).(subst0 i u0 u u2))) (ex2 T (\lambda (t6: T).(eq T t5 (THead
+(Bind b) u t6))) (\lambda (t6: T).(subst0 (s (Bind b) i) u0 t2 t6))) (ex3_2 T
+T (\lambda (u2: T).(\lambda (t6: T).(eq T t5 (THead (Bind b) u2 t6))))