-T).(\lambda (H: (ty3 g c (THead (Flat Appl) w v) x)).(let TMP_5 \def (\lambda
-(u: T).(\lambda (t: T).(let TMP_1 \def (Flat Appl) in (let TMP_2 \def (Bind
-Abst) in (let TMP_3 \def (THead TMP_2 u t) in (let TMP_4 \def (THead TMP_1 w
-TMP_3) in (pc3 c TMP_4 x))))))) in (let TMP_8 \def (\lambda (u: T).(\lambda
-(t: T).(let TMP_6 \def (Bind Abst) in (let TMP_7 \def (THead TMP_6 u t) in
-(ty3 g c v TMP_7))))) in (let TMP_9 \def (\lambda (u: T).(\lambda (_: T).(ty3
-g c w u))) in (let TMP_14 \def (\lambda (u: T).(\lambda (t: T).(let TMP_10
-\def (Flat Appl) in (let TMP_11 \def (Bind Abst) in (let TMP_12 \def (THead
-TMP_11 u t) in (let TMP_13 \def (THead TMP_10 w TMP_12) in (pc3 c TMP_13
-x))))))) in (let TMP_17 \def (\lambda (u: T).(\lambda (t: T).(let TMP_15 \def
-(Bind Abst) in (let TMP_16 \def (THead TMP_15 u t) in (ty3 g c v TMP_16)))))
-in (let TMP_18 \def (\lambda (u: T).(\lambda (_: T).(ty3 g c w u))) in (let
-TMP_21 \def (\lambda (u: T).(\lambda (t: T).(let TMP_19 \def (Bind Abst) in
-(let TMP_20 \def (THead TMP_19 u t) in (nf2 c TMP_20))))) in (let TMP_22 \def
-(ex4_2 T T TMP_14 TMP_17 TMP_18 TMP_21) in (let TMP_149 \def (\lambda (x0:
-T).(\lambda (x1: T).(\lambda (H0: (pc3 c (THead (Flat Appl) w (THead (Bind
-Abst) x0 x1)) x)).(\lambda (H1: (ty3 g c v (THead (Bind Abst) x0
-x1))).(\lambda (H2: (ty3 g c w x0)).(let TMP_23 \def (Bind Abst) in (let
-TMP_24 \def (THead TMP_23 x0 x1) in (let H_x \def (ty3_correct g c v TMP_24
-H1) in (let H3 \def H_x in (let TMP_27 \def (\lambda (t: T).(let TMP_25 \def
-(Bind Abst) in (let TMP_26 \def (THead TMP_25 x0 x1) in (ty3 g c TMP_26 t))))
-in (let TMP_32 \def (\lambda (u: T).(\lambda (t: T).(let TMP_28 \def (Flat
-Appl) in (let TMP_29 \def (Bind Abst) in (let TMP_30 \def (THead TMP_29 u t)
-in (let TMP_31 \def (THead TMP_28 w TMP_30) in (pc3 c TMP_31 x))))))) in (let
-TMP_35 \def (\lambda (u: T).(\lambda (t: T).(let TMP_33 \def (Bind Abst) in
-(let TMP_34 \def (THead TMP_33 u t) in (ty3 g c v TMP_34))))) in (let TMP_36
-\def (\lambda (u: T).(\lambda (_: T).(ty3 g c w u))) in (let TMP_39 \def
-(\lambda (u: T).(\lambda (t: T).(let TMP_37 \def (Bind Abst) in (let TMP_38
-\def (THead TMP_37 u t) in (nf2 c TMP_38))))) in (let TMP_40 \def (ex4_2 T T
-TMP_32 TMP_35 TMP_36 TMP_39) in (let TMP_148 \def (\lambda (x2: T).(\lambda
-(H4: (ty3 g c (THead (Bind Abst) x0 x1) x2)).(let H_x0 \def (ty3_correct g c
-w x0 H2) in (let H5 \def H_x0 in (let TMP_41 \def (\lambda (t: T).(ty3 g c x0
-t)) in (let TMP_46 \def (\lambda (u: T).(\lambda (t: T).(let TMP_42 \def
-(Flat Appl) in (let TMP_43 \def (Bind Abst) in (let TMP_44 \def (THead TMP_43
-u t) in (let TMP_45 \def (THead TMP_42 w TMP_44) in (pc3 c TMP_45 x))))))) in
-(let TMP_49 \def (\lambda (u: T).(\lambda (t: T).(let TMP_47 \def (Bind Abst)
-in (let TMP_48 \def (THead TMP_47 u t) in (ty3 g c v TMP_48))))) in (let
-TMP_50 \def (\lambda (u: T).(\lambda (_: T).(ty3 g c w u))) in (let TMP_53
-\def (\lambda (u: T).(\lambda (t: T).(let TMP_51 \def (Bind Abst) in (let
-TMP_52 \def (THead TMP_51 u t) in (nf2 c TMP_52))))) in (let TMP_54 \def
-(ex4_2 T T TMP_46 TMP_49 TMP_50 TMP_53) in (let TMP_147 \def (\lambda (x3:
-T).(\lambda (H6: (ty3 g c x0 x3)).(let TMP_55 \def (Bind Abst) in (let TMP_56
-\def (THead TMP_55 x0 x1) in (let H7 \def (ty3_sn3 g c TMP_56 x2 H4) in (let
-TMP_57 \def (Bind Abst) in (let TMP_58 \def (THead TMP_57 x0 x1) in (let H_x1
-\def (nf2_sn3 c TMP_58 H7) in (let H8 \def H_x1 in (let TMP_61 \def (\lambda
-(u: T).(let TMP_59 \def (Bind Abst) in (let TMP_60 \def (THead TMP_59 x0 x1)
-in (pr3 c TMP_60 u)))) in (let TMP_62 \def (\lambda (u: T).(nf2 c u)) in (let
-TMP_67 \def (\lambda (u: T).(\lambda (t: T).(let TMP_63 \def (Flat Appl) in
-(let TMP_64 \def (Bind Abst) in (let TMP_65 \def (THead TMP_64 u t) in (let
-TMP_66 \def (THead TMP_63 w TMP_65) in (pc3 c TMP_66 x))))))) in (let TMP_70
-\def (\lambda (u: T).(\lambda (t: T).(let TMP_68 \def (Bind Abst) in (let
-TMP_69 \def (THead TMP_68 u t) in (ty3 g c v TMP_69))))) in (let TMP_71 \def
-(\lambda (u: T).(\lambda (_: T).(ty3 g c w u))) in (let TMP_74 \def (\lambda
-(u: T).(\lambda (t: T).(let TMP_72 \def (Bind Abst) in (let TMP_73 \def
-(THead TMP_72 u t) in (nf2 c TMP_73))))) in (let TMP_75 \def (ex4_2 T T
-TMP_67 TMP_70 TMP_71 TMP_74) in (let TMP_146 \def (\lambda (x4: T).(\lambda
-(H9: (pr3 c (THead (Bind Abst) x0 x1) x4)).(\lambda (H10: (nf2 c x4)).(let
-H11 \def (pr3_gen_abst c x0 x1 x4 H9) in (let TMP_78 \def (\lambda (u2:
-T).(\lambda (t2: T).(let TMP_76 \def (Bind Abst) in (let TMP_77 \def (THead
-TMP_76 u2 t2) in (eq T x4 TMP_77))))) in (let TMP_79 \def (\lambda (u2:
-T).(\lambda (_: T).(pr3 c x0 u2))) in (let TMP_82 \def (\lambda (_:
-T).(\lambda (t2: T).(\forall (b: B).(\forall (u: T).(let TMP_80 \def (Bind b)
-in (let TMP_81 \def (CHead c TMP_80 u) in (pr3 TMP_81 x1 t2))))))) in (let
-TMP_87 \def (\lambda (u: T).(\lambda (t: T).(let TMP_83 \def (Flat Appl) in
-(let TMP_84 \def (Bind Abst) in (let TMP_85 \def (THead TMP_84 u t) in (let
-TMP_86 \def (THead TMP_83 w TMP_85) in (pc3 c TMP_86 x))))))) in (let TMP_90
-\def (\lambda (u: T).(\lambda (t: T).(let TMP_88 \def (Bind Abst) in (let
-TMP_89 \def (THead TMP_88 u t) in (ty3 g c v TMP_89))))) in (let TMP_91 \def
-(\lambda (u: T).(\lambda (_: T).(ty3 g c w u))) in (let TMP_94 \def (\lambda
-(u: T).(\lambda (t: T).(let TMP_92 \def (Bind Abst) in (let TMP_93 \def
-(THead TMP_92 u t) in (nf2 c TMP_93))))) in (let TMP_95 \def (ex4_2 T T
-TMP_87 TMP_90 TMP_91 TMP_94) in (let TMP_145 \def (\lambda (x5: T).(\lambda
-(x6: T).(\lambda (H12: (eq T x4 (THead (Bind Abst) x5 x6))).(\lambda (H13:
-(pr3 c x0 x5)).(\lambda (H14: ((\forall (b: B).(\forall (u: T).(pr3 (CHead c
-(Bind b) u) x1 x6))))).(let TMP_96 \def (\lambda (t: T).(nf2 c t)) in (let
-TMP_97 \def (Bind Abst) in (let TMP_98 \def (THead TMP_97 x5 x6) in (let H15
-\def (eq_ind T x4 TMP_96 H10 TMP_98 H12) in (let TMP_99 \def (Bind Abst) in
-(let TMP_100 \def (H14 Abst x5) in (let H16 \def (pr3_head_12 c x0 x5 H13
-TMP_99 x1 x6 TMP_100) in (let TMP_105 \def (\lambda (u: T).(\lambda (t:
-T).(let TMP_101 \def (Flat Appl) in (let TMP_102 \def (Bind Abst) in (let
-TMP_103 \def (THead TMP_102 u t) in (let TMP_104 \def (THead TMP_101 w
-TMP_103) in (pc3 c TMP_104 x))))))) in (let TMP_108 \def (\lambda (u:
-T).(\lambda (t: T).(let TMP_106 \def (Bind Abst) in (let TMP_107 \def (THead
-TMP_106 u t) in (ty3 g c v TMP_107))))) in (let TMP_109 \def (\lambda (u:
-T).(\lambda (_: T).(ty3 g c w u))) in (let TMP_112 \def (\lambda (u:
-T).(\lambda (t: T).(let TMP_110 \def (Bind Abst) in (let TMP_111 \def (THead
-TMP_110 u t) in (nf2 c TMP_111))))) in (let TMP_113 \def (Flat Appl) in (let
-TMP_114 \def (Bind Abst) in (let TMP_115 \def (THead TMP_114 x0 x1) in (let
-TMP_116 \def (THead TMP_113 w TMP_115) in (let TMP_117 \def (Flat Appl) in
-(let TMP_118 \def (Bind Abst) in (let TMP_119 \def (THead TMP_118 x5 x6) in
-(let TMP_120 \def (THead TMP_117 w TMP_119) in (let TMP_121 \def (Bind Abst)
-in (let TMP_122 \def (THead TMP_121 x0 x1) in (let TMP_123 \def (Bind Abst)
-in (let TMP_124 \def (THead TMP_123 x5 x6) in (let TMP_125 \def (pr3_thin_dx
-c TMP_122 TMP_124 H16 w Appl) in (let TMP_126 \def (pc3_pr3_conf c TMP_116 x
-H0 TMP_120 TMP_125) in (let TMP_127 \def (Bind Abst) in (let TMP_128 \def
-(THead TMP_127 x5 x6) in (let TMP_129 \def (Bind Abst) in (let TMP_130 \def
-(THead TMP_129 x0 x1) in (let TMP_131 \def (Bind Abst) in (let TMP_132 \def
-(THead TMP_131 x5 x6) in (let TMP_133 \def (ty3_sred_pr3 c TMP_130 TMP_132
-H16 g x2 H4) in (let TMP_134 \def (Bind Abst) in (let TMP_135 \def (THead
-TMP_134 x0 x1) in (let TMP_136 \def (Bind Abst) in (let TMP_137 \def (THead
-TMP_136 x0 x1) in (let TMP_138 \def (Bind Abst) in (let TMP_139 \def (THead
-TMP_138 x5 x6) in (let TMP_140 \def (pc3_pr3_r c TMP_137 TMP_139 H16) in (let
-TMP_141 \def (ty3_conv g c TMP_128 x2 TMP_133 v TMP_135 H1 TMP_140) in (let
-TMP_142 \def (ty3_sred_pr3 c x0 x5 H13 g x3 H6) in (let TMP_143 \def
-(pc3_pr3_r c x0 x5 H13) in (let TMP_144 \def (ty3_conv g c x5 x3 TMP_142 w x0
-H2 TMP_143) in (ex4_2_intro T T TMP_105 TMP_108 TMP_109 TMP_112 x5 x6 TMP_126
-TMP_141 TMP_144 H15))))))))))))))))))))))))))))))))))))))))))))))))) in
-(ex3_2_ind T T TMP_78 TMP_79 TMP_82 TMP_95 TMP_145 H11)))))))))))))) in
-(ex2_ind T TMP_61 TMP_62 TMP_75 TMP_146 H8)))))))))))))))))) in (ex_ind T
-TMP_41 TMP_54 TMP_147 H5)))))))))))) in (ex_ind T TMP_27 TMP_40 TMP_148
-H3))))))))))))))))) in (let TMP_150 \def (ty3_gen_appl g c w v x H) in
-(ex3_2_ind T T TMP_5 TMP_8 TMP_9 TMP_22 TMP_149 TMP_150)))))))))))))))).
+T).(\lambda (H: (ty3 g c (THead (Flat Appl) w v) x)).(ex3_2_ind T T (\lambda
+(u: T).(\lambda (t: T).(pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t))
+x))) (\lambda (u: T).(\lambda (t: T).(ty3 g c v (THead (Bind Abst) u t))))
+(\lambda (u: T).(\lambda (_: T).(ty3 g c w u))) (ex4_2 T T (\lambda (u:
+T).(\lambda (t: T).(pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x)))
+(\lambda (u: T).(\lambda (t: T).(ty3 g c v (THead (Bind Abst) u t))))
+(\lambda (u: T).(\lambda (_: T).(ty3 g c w u))) (\lambda (u: T).(\lambda (t:
+T).(nf2 c (THead (Bind Abst) u t))))) (\lambda (x0: T).(\lambda (x1:
+T).(\lambda (H0: (pc3 c (THead (Flat Appl) w (THead (Bind Abst) x0 x1))
+x)).(\lambda (H1: (ty3 g c v (THead (Bind Abst) x0 x1))).(\lambda (H2: (ty3 g
+c w x0)).(let H_x \def (ty3_correct g c v (THead (Bind Abst) x0 x1) H1) in
+(let H3 \def H_x in (ex_ind T (\lambda (t: T).(ty3 g c (THead (Bind Abst) x0
+x1) t)) (ex4_2 T T (\lambda (u: T).(\lambda (t: T).(pc3 c (THead (Flat Appl)
+w (THead (Bind Abst) u t)) x))) (\lambda (u: T).(\lambda (t: T).(ty3 g c v
+(THead (Bind Abst) u t)))) (\lambda (u: T).(\lambda (_: T).(ty3 g c w u)))
+(\lambda (u: T).(\lambda (t: T).(nf2 c (THead (Bind Abst) u t))))) (\lambda
+(x2: T).(\lambda (H4: (ty3 g c (THead (Bind Abst) x0 x1) x2)).(let H_x0 \def
+(ty3_correct g c w x0 H2) in (let H5 \def H_x0 in (ex_ind T (\lambda (t:
+T).(ty3 g c x0 t)) (ex4_2 T T (\lambda (u: T).(\lambda (t: T).(pc3 c (THead
+(Flat Appl) w (THead (Bind Abst) u t)) x))) (\lambda (u: T).(\lambda (t:
+T).(ty3 g c v (THead (Bind Abst) u t)))) (\lambda (u: T).(\lambda (_: T).(ty3
+g c w u))) (\lambda (u: T).(\lambda (t: T).(nf2 c (THead (Bind Abst) u t)))))
+(\lambda (x3: T).(\lambda (H6: (ty3 g c x0 x3)).(let H7 \def (ty3_sn3 g c
+(THead (Bind Abst) x0 x1) x2 H4) in (let H_x1 \def (nf2_sn3 c (THead (Bind
+Abst) x0 x1) H7) in (let H8 \def H_x1 in (ex2_ind T (\lambda (u: T).(pr3 c
+(THead (Bind Abst) x0 x1) u)) (\lambda (u: T).(nf2 c u)) (ex4_2 T T (\lambda
+(u: T).(\lambda (t: T).(pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t))
+x))) (\lambda (u: T).(\lambda (t: T).(ty3 g c v (THead (Bind Abst) u t))))
+(\lambda (u: T).(\lambda (_: T).(ty3 g c w u))) (\lambda (u: T).(\lambda (t:
+T).(nf2 c (THead (Bind Abst) u t))))) (\lambda (x4: T).(\lambda (H9: (pr3 c
+(THead (Bind Abst) x0 x1) x4)).(\lambda (H10: (nf2 c x4)).(let H11 \def
+(pr3_gen_abst c x0 x1 x4 H9) in (ex3_2_ind T T (\lambda (u2: T).(\lambda (t2:
+T).(eq T x4 (THead (Bind Abst) u2 t2)))) (\lambda (u2: T).(\lambda (_:
+T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t2: T).(\forall (b: B).(\forall
+(u: T).(pr3 (CHead c (Bind b) u) x1 t2))))) (ex4_2 T T (\lambda (u:
+T).(\lambda (t: T).(pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x)))
+(\lambda (u: T).(\lambda (t: T).(ty3 g c v (THead (Bind Abst) u t))))
+(\lambda (u: T).(\lambda (_: T).(ty3 g c w u))) (\lambda (u: T).(\lambda (t:
+T).(nf2 c (THead (Bind Abst) u t))))) (\lambda (x5: T).(\lambda (x6:
+T).(\lambda (H12: (eq T x4 (THead (Bind Abst) x5 x6))).(\lambda (H13: (pr3 c
+x0 x5)).(\lambda (H14: ((\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind
+b) u) x1 x6))))).(let H15 \def (eq_ind T x4 (\lambda (t: T).(nf2 c t)) H10
+(THead (Bind Abst) x5 x6) H12) in (let H16 \def (pr3_head_12 c x0 x5 H13
+(Bind Abst) x1 x6 (H14 Abst x5)) in (ex4_2_intro T T (\lambda (u: T).(\lambda
+(t: T).(pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x))) (\lambda (u:
+T).(\lambda (t: T).(ty3 g c v (THead (Bind Abst) u t)))) (\lambda (u:
+T).(\lambda (_: T).(ty3 g c w u))) (\lambda (u: T).(\lambda (t: T).(nf2 c
+(THead (Bind Abst) u t)))) x5 x6 (pc3_pr3_conf c (THead (Flat Appl) w (THead
+(Bind Abst) x0 x1)) x H0 (THead (Flat Appl) w (THead (Bind Abst) x5 x6))
+(pr3_thin_dx c (THead (Bind Abst) x0 x1) (THead (Bind Abst) x5 x6) H16 w
+Appl)) (ty3_conv g c (THead (Bind Abst) x5 x6) x2 (ty3_sred_pr3 c (THead
+(Bind Abst) x0 x1) (THead (Bind Abst) x5 x6) H16 g x2 H4) v (THead (Bind
+Abst) x0 x1) H1 (pc3_pr3_r c (THead (Bind Abst) x0 x1) (THead (Bind Abst) x5
+x6) H16)) (ty3_conv g c x5 x3 (ty3_sred_pr3 c x0 x5 H13 g x3 H6) w x0 H2
+(pc3_pr3_r c x0 x5 H13)) H15)))))))) H11))))) H8)))))) H5))))) H3))))))))
+(ty3_gen_appl g c w v x H))))))).