-(let TMP_64 \def (\lambda (t4: T).(let TMP_62 \def (Bind b) in (let TMP_63
-\def (CHead c0 TMP_62 v) in (sty1 g TMP_63 t2 t4)))) in (let TMP_65 \def
-(\lambda (t4: T).(cnt t4)) in (let TMP_68 \def (\lambda (t4: T).(let TMP_66
-\def (Bind b) in (let TMP_67 \def (THead TMP_66 v t2) in (sty1 g c0 TMP_67
-t4)))) in (let TMP_69 \def (\lambda (t4: T).(cnt t4)) in (let TMP_70 \def
-(ex2 T TMP_68 TMP_69) in (let TMP_80 \def (\lambda (x: T).(\lambda (H3: (sty1
-g (CHead c0 (Bind b) v) t2 x)).(\lambda (H4: (cnt x)).(let TMP_73 \def
-(\lambda (t4: T).(let TMP_71 \def (Bind b) in (let TMP_72 \def (THead TMP_71
-v t2) in (sty1 g c0 TMP_72 t4)))) in (let TMP_74 \def (\lambda (t4: T).(cnt
-t4)) in (let TMP_75 \def (Bind b) in (let TMP_76 \def (THead TMP_75 v x) in
-(let TMP_77 \def (sty1_bind g b c0 v t2 x H3) in (let TMP_78 \def (Bind b) in
-(let TMP_79 \def (cnt_head x H4 TMP_78 v) in (ex_intro2 T TMP_73 TMP_74
-TMP_76 TMP_77 TMP_79))))))))))) in (ex2_ind T TMP_64 TMP_65 TMP_70 TMP_80
-H2))))))))))))))) in (let TMP_99 \def (\lambda (c0: C).(\lambda (v:
-T).(\lambda (t2: T).(\lambda (t3: T).(\lambda (_: (sty0 g c0 t2 t3)).(\lambda
-(H1: (ex2 T (\lambda (t4: T).(sty1 g c0 t2 t4)) (\lambda (t4: T).(cnt
-t4)))).(let H2 \def H1 in (let TMP_82 \def (\lambda (t4: T).(sty1 g c0 t2
-t4)) in (let TMP_83 \def (\lambda (t4: T).(cnt t4)) in (let TMP_86 \def
-(\lambda (t4: T).(let TMP_84 \def (Flat Appl) in (let TMP_85 \def (THead
-TMP_84 v t2) in (sty1 g c0 TMP_85 t4)))) in (let TMP_87 \def (\lambda (t4:
-T).(cnt t4)) in (let TMP_88 \def (ex2 T TMP_86 TMP_87) in (let TMP_98 \def
-(\lambda (x: T).(\lambda (H3: (sty1 g c0 t2 x)).(\lambda (H4: (cnt x)).(let
-TMP_91 \def (\lambda (t4: T).(let TMP_89 \def (Flat Appl) in (let TMP_90 \def
-(THead TMP_89 v t2) in (sty1 g c0 TMP_90 t4)))) in (let TMP_92 \def (\lambda
-(t4: T).(cnt t4)) in (let TMP_93 \def (Flat Appl) in (let TMP_94 \def (THead
-TMP_93 v x) in (let TMP_95 \def (sty1_appl g c0 v t2 x H3) in (let TMP_96
-\def (Flat Appl) in (let TMP_97 \def (cnt_head x H4 TMP_96 v) in (ex_intro2 T
-TMP_91 TMP_92 TMP_94 TMP_95 TMP_97))))))))))) in (ex2_ind T TMP_82 TMP_83
-TMP_88 TMP_98 H2)))))))))))))) in (let TMP_128 \def (\lambda (c0: C).(\lambda
-(v1: T).(\lambda (v2: T).(\lambda (H0: (sty0 g c0 v1 v2)).(\lambda (_: (ex2 T
-(\lambda (t2: T).(sty1 g c0 v1 t2)) (\lambda (t2: T).(cnt t2)))).(\lambda
-(t2: T).(\lambda (t3: T).(\lambda (_: (sty0 g c0 t2 t3)).(\lambda (H3: (ex2 T
-(\lambda (t4: T).(sty1 g c0 t2 t4)) (\lambda (t4: T).(cnt t4)))).(let H4 \def
-H3 in (let TMP_100 \def (\lambda (t4: T).(sty1 g c0 t2 t4)) in (let TMP_101
-\def (\lambda (t4: T).(cnt t4)) in (let TMP_104 \def (\lambda (t4: T).(let
-TMP_102 \def (Flat Cast) in (let TMP_103 \def (THead TMP_102 v1 t2) in (sty1
-g c0 TMP_103 t4)))) in (let TMP_105 \def (\lambda (t4: T).(cnt t4)) in (let
-TMP_106 \def (ex2 T TMP_104 TMP_105) in (let TMP_127 \def (\lambda (x:
-T).(\lambda (H5: (sty1 g c0 t2 x)).(\lambda (H6: (cnt x)).(let H_x \def
-(sty1_cast2 g c0 t2 x H5 v1 v2 H0) in (let H7 \def H_x in (let TMP_107 \def
-(\lambda (v3: T).(sty1 g c0 v1 v3)) in (let TMP_112 \def (\lambda (v3:
-T).(let TMP_108 \def (Flat Cast) in (let TMP_109 \def (THead TMP_108 v1 t2)
-in (let TMP_110 \def (Flat Cast) in (let TMP_111 \def (THead TMP_110 v3 x) in
-(sty1 g c0 TMP_109 TMP_111)))))) in (let TMP_115 \def (\lambda (t4: T).(let
-TMP_113 \def (Flat Cast) in (let TMP_114 \def (THead TMP_113 v1 t2) in (sty1
-g c0 TMP_114 t4)))) in (let TMP_116 \def (\lambda (t4: T).(cnt t4)) in (let
-TMP_117 \def (ex2 T TMP_115 TMP_116) in (let TMP_126 \def (\lambda (x0:
-T).(\lambda (_: (sty1 g c0 v1 x0)).(\lambda (H9: (sty1 g c0 (THead (Flat
-Cast) v1 t2) (THead (Flat Cast) x0 x))).(let TMP_120 \def (\lambda (t4:
-T).(let TMP_118 \def (Flat Cast) in (let TMP_119 \def (THead TMP_118 v1 t2)
-in (sty1 g c0 TMP_119 t4)))) in (let TMP_121 \def (\lambda (t4: T).(cnt t4))
-in (let TMP_122 \def (Flat Cast) in (let TMP_123 \def (THead TMP_122 x0 x) in
-(let TMP_124 \def (Flat Cast) in (let TMP_125 \def (cnt_head x H6 TMP_124 x0)
-in (ex_intro2 T TMP_120 TMP_121 TMP_123 H9 TMP_125)))))))))) in (ex2_ind T
-TMP_107 TMP_112 TMP_117 TMP_126 H7)))))))))))) in (ex2_ind T TMP_100 TMP_101
-TMP_106 TMP_127 H4))))))))))))))))) in (sty0_ind g TMP_3 TMP_16 TMP_32 TMP_61
-TMP_81 TMP_99 TMP_128 c t1 t H)))))))))))).
+(ex2_ind T (\lambda (t4: T).(sty1 g (CHead c0 (Bind b) v) t2 t4)) (\lambda
+(t4: T).(cnt t4)) (ex2 T (\lambda (t4: T).(sty1 g c0 (THead (Bind b) v t2)
+t4)) (\lambda (t4: T).(cnt t4))) (\lambda (x: T).(\lambda (H3: (sty1 g (CHead
+c0 (Bind b) v) t2 x)).(\lambda (H4: (cnt x)).(ex_intro2 T (\lambda (t4:
+T).(sty1 g c0 (THead (Bind b) v t2) t4)) (\lambda (t4: T).(cnt t4)) (THead
+(Bind b) v x) (sty1_bind g b c0 v t2 x H3) (cnt_head x H4 (Bind b) v)))))
+H2))))))))) (\lambda (c0: C).(\lambda (v: T).(\lambda (t2: T).(\lambda (t3:
+T).(\lambda (_: (sty0 g c0 t2 t3)).(\lambda (H1: (ex2 T (\lambda (t4:
+T).(sty1 g c0 t2 t4)) (\lambda (t4: T).(cnt t4)))).(let H2 \def H1 in
+(ex2_ind T (\lambda (t4: T).(sty1 g c0 t2 t4)) (\lambda (t4: T).(cnt t4))
+(ex2 T (\lambda (t4: T).(sty1 g c0 (THead (Flat Appl) v t2) t4)) (\lambda
+(t4: T).(cnt t4))) (\lambda (x: T).(\lambda (H3: (sty1 g c0 t2 x)).(\lambda
+(H4: (cnt x)).(ex_intro2 T (\lambda (t4: T).(sty1 g c0 (THead (Flat Appl) v
+t2) t4)) (\lambda (t4: T).(cnt t4)) (THead (Flat Appl) v x) (sty1_appl g c0 v
+t2 x H3) (cnt_head x H4 (Flat Appl) v))))) H2)))))))) (\lambda (c0:
+C).(\lambda (v1: T).(\lambda (v2: T).(\lambda (H0: (sty0 g c0 v1
+v2)).(\lambda (_: (ex2 T (\lambda (t2: T).(sty1 g c0 v1 t2)) (\lambda (t2:
+T).(cnt t2)))).(\lambda (t2: T).(\lambda (t3: T).(\lambda (_: (sty0 g c0 t2
+t3)).(\lambda (H3: (ex2 T (\lambda (t4: T).(sty1 g c0 t2 t4)) (\lambda (t4:
+T).(cnt t4)))).(let H4 \def H3 in (ex2_ind T (\lambda (t4: T).(sty1 g c0 t2
+t4)) (\lambda (t4: T).(cnt t4)) (ex2 T (\lambda (t4: T).(sty1 g c0 (THead
+(Flat Cast) v1 t2) t4)) (\lambda (t4: T).(cnt t4))) (\lambda (x: T).(\lambda
+(H5: (sty1 g c0 t2 x)).(\lambda (H6: (cnt x)).(let H_x \def (sty1_cast2 g c0
+t2 x H5 v1 v2 H0) in (let H7 \def H_x in (ex2_ind T (\lambda (v3: T).(sty1 g
+c0 v1 v3)) (\lambda (v3: T).(sty1 g c0 (THead (Flat Cast) v1 t2) (THead (Flat
+Cast) v3 x))) (ex2 T (\lambda (t4: T).(sty1 g c0 (THead (Flat Cast) v1 t2)
+t4)) (\lambda (t4: T).(cnt t4))) (\lambda (x0: T).(\lambda (_: (sty1 g c0 v1
+x0)).(\lambda (H9: (sty1 g c0 (THead (Flat Cast) v1 t2) (THead (Flat Cast) x0
+x))).(ex_intro2 T (\lambda (t4: T).(sty1 g c0 (THead (Flat Cast) v1 t2) t4))
+(\lambda (t4: T).(cnt t4)) (THead (Flat Cast) x0 x) H9 (cnt_head x H6 (Flat
+Cast) x0))))) H7)))))) H4))))))))))) c t1 t H))))).