+T).(\lambda (_: F).(\lambda (H3: (eq C c2 (CHead c k v))).(let TMP_91 \def
+(\lambda (e: C).e) in (let TMP_92 \def (CHead c k v) in (let H4 \def (f_equal
+C C TMP_91 c2 TMP_92 H3) in (let TMP_95 \def (\lambda (c0: C).((eq C c0
+(CHead c k v)) \to (let TMP_94 \def (\lambda (b: B).(let TMP_93 \def (Bind b)
+in (eq K k TMP_93))) in (ex B TMP_94)))) in (let TMP_96 \def (CHead c k v) in
+(let H5 \def (eq_ind C c2 TMP_95 H2 TMP_96 H4) in (let TMP_97 \def (\lambda
+(c0: C).(wf3 g c1 c0)) in (let TMP_98 \def (CHead c k v) in (let H6 \def
+(eq_ind C c2 TMP_97 H1 TMP_98 H4) in (let TMP_99 \def (CHead c k v) in (let
+TMP_100 \def (refl_equal C TMP_99) in (H5 TMP_100))))))))))))))))))) in
+(wf3_ind g TMP_8 TMP_15 TMP_49 TMP_90 TMP_101 x y H0)))))))) in (insert_eq C
+TMP_1 TMP_2 TMP_5 TMP_102 H)))))))))).
+
+theorem wf3_mono:
+ \forall (g: G).(\forall (c: C).(\forall (c1: C).((wf3 g c c1) \to (\forall
+(c2: C).((wf3 g c c2) \to (eq C c1 c2))))))
+\def
+ \lambda (g: G).(\lambda (c: C).(\lambda (c1: C).(\lambda (H: (wf3 g c
+c1)).(let TMP_1 \def (\lambda (c0: C).(\lambda (c2: C).(\forall (c3: C).((wf3
+g c0 c3) \to (eq C c2 c3))))) in (let TMP_7 \def (\lambda (m: nat).(\lambda
+(c2: C).(\lambda (H0: (wf3 g (CSort m) c2)).(let H_y \def (wf3_gen_sort1 g c2
+m H0) in (let TMP_2 \def (CSort m) in (let TMP_4 \def (\lambda (c0: C).(let
+TMP_3 \def (CSort m) in (eq C TMP_3 c0))) in (let TMP_5 \def (CSort m) in
+(let TMP_6 \def (refl_equal C TMP_5) in (eq_ind_r C TMP_2 TMP_4 TMP_6 c2
+H_y))))))))) in (let TMP_70 \def (\lambda (c2: C).(\lambda (c3: C).(\lambda
+(_: (wf3 g c2 c3)).(\lambda (H1: ((\forall (c4: C).((wf3 g c2 c4) \to (eq C
+c3 c4))))).(\lambda (u: T).(\lambda (t: T).(\lambda (H2: (ty3 g c2 u
+t)).(\lambda (b: B).(\lambda (c0: C).(\lambda (H3: (wf3 g (CHead c2 (Bind b)
+u) c0)).(let H_x \def (wf3_gen_bind1 g c2 c0 u b H3) in (let H4 \def H_x in
+(let TMP_10 \def (\lambda (c4: C).(\lambda (_: T).(let TMP_8 \def (Bind b) in
+(let TMP_9 \def (CHead c4 TMP_8 u) in (eq C c0 TMP_9))))) in (let TMP_11 \def
+(\lambda (c4: C).(\lambda (_: T).(wf3 g c2 c4))) in (let TMP_12 \def (\lambda
+(_: C).(\lambda (w: T).(ty3 g c2 u w))) in (let TMP_13 \def (ex3_2 C T TMP_10
+TMP_11 TMP_12) in (let TMP_17 \def (\lambda (c4: C).(let TMP_14 \def (Bind
+Void) in (let TMP_15 \def (TSort O) in (let TMP_16 \def (CHead c4 TMP_14
+TMP_15) in (eq C c0 TMP_16))))) in (let TMP_18 \def (\lambda (c4: C).(wf3 g
+c2 c4)) in (let TMP_19 \def (\lambda (_: C).(\forall (w: T).((ty3 g c2 u w)
+\to False))) in (let TMP_20 \def (ex3 C TMP_17 TMP_18 TMP_19) in (let TMP_21
+\def (Bind b) in (let TMP_22 \def (CHead c3 TMP_21 u) in (let TMP_23 \def (eq
+C TMP_22 c0) in (let TMP_45 \def (\lambda (H5: (ex3_2 C T (\lambda (c4:
+C).(\lambda (_: T).(eq C c0 (CHead c4 (Bind b) u)))) (\lambda (c4:
+C).(\lambda (_: T).(wf3 g c2 c4))) (\lambda (_: C).(\lambda (w: T).(ty3 g c2
+u w))))).(let TMP_26 \def (\lambda (c4: C).(\lambda (_: T).(let TMP_24 \def
+(Bind b) in (let TMP_25 \def (CHead c4 TMP_24 u) in (eq C c0 TMP_25))))) in
+(let TMP_27 \def (\lambda (c4: C).(\lambda (_: T).(wf3 g c2 c4))) in (let
+TMP_28 \def (\lambda (_: C).(\lambda (w: T).(ty3 g c2 u w))) in (let TMP_29
+\def (Bind b) in (let TMP_30 \def (CHead c3 TMP_29 u) in (let TMP_31 \def (eq
+C TMP_30 c0) in (let TMP_44 \def (\lambda (x0: C).(\lambda (x1: T).(\lambda
+(H6: (eq C c0 (CHead x0 (Bind b) u))).(\lambda (H7: (wf3 g c2 x0)).(\lambda
+(_: (ty3 g c2 u x1)).(let TMP_32 \def (Bind b) in (let TMP_33 \def (CHead x0
+TMP_32 u) in (let TMP_36 \def (\lambda (c4: C).(let TMP_34 \def (Bind b) in
+(let TMP_35 \def (CHead c3 TMP_34 u) in (eq C TMP_35 c4)))) in (let TMP_37
+\def (Bind b) in (let TMP_38 \def (Bind b) in (let TMP_39 \def (H1 x0 H7) in
+(let TMP_40 \def (Bind b) in (let TMP_41 \def (refl_equal K TMP_40) in (let
+TMP_42 \def (refl_equal T u) in (let TMP_43 \def (f_equal3 C K T C CHead c3
+x0 TMP_37 TMP_38 u u TMP_39 TMP_41 TMP_42) in (eq_ind_r C TMP_33 TMP_36
+TMP_43 c0 H6)))))))))))))))) in (ex3_2_ind C T TMP_26 TMP_27 TMP_28 TMP_31
+TMP_44 H5))))))))) in (let TMP_69 \def (\lambda (H5: (ex3 C (\lambda (c4:
+C).(eq C c0 (CHead c4 (Bind Void) (TSort O)))) (\lambda (c4: C).(wf3 g c2
+c4)) (\lambda (_: C).(\forall (w: T).((ty3 g c2 u w) \to False))))).(let
+TMP_49 \def (\lambda (c4: C).(let TMP_46 \def (Bind Void) in (let TMP_47 \def
+(TSort O) in (let TMP_48 \def (CHead c4 TMP_46 TMP_47) in (eq C c0
+TMP_48))))) in (let TMP_50 \def (\lambda (c4: C).(wf3 g c2 c4)) in (let
+TMP_51 \def (\lambda (_: C).(\forall (w: T).((ty3 g c2 u w) \to False))) in
+(let TMP_52 \def (Bind b) in (let TMP_53 \def (CHead c3 TMP_52 u) in (let
+TMP_54 \def (eq C TMP_53 c0) in (let TMP_68 \def (\lambda (x0: C).(\lambda
+(H6: (eq C c0 (CHead x0 (Bind Void) (TSort O)))).(\lambda (_: (wf3 g c2
+x0)).(\lambda (H8: ((\forall (w: T).((ty3 g c2 u w) \to False)))).(let TMP_55
+\def (Bind Void) in (let TMP_56 \def (TSort O) in (let TMP_57 \def (CHead x0
+TMP_55 TMP_56) in (let TMP_60 \def (\lambda (c4: C).(let TMP_58 \def (Bind b)
+in (let TMP_59 \def (CHead c3 TMP_58 u) in (eq C TMP_59 c4)))) in (let H_x0
+\def (H8 t H2) in (let H9 \def H_x0 in (let TMP_61 \def (Bind b) in (let
+TMP_62 \def (CHead c3 TMP_61 u) in (let TMP_63 \def (Bind Void) in (let
+TMP_64 \def (TSort O) in (let TMP_65 \def (CHead x0 TMP_63 TMP_64) in (let
+TMP_66 \def (eq C TMP_62 TMP_65) in (let TMP_67 \def (False_ind TMP_66 H9) in
+(eq_ind_r C TMP_57 TMP_60 TMP_67 c0 H6)))))))))))))))))) in (ex3_ind C TMP_49
+TMP_50 TMP_51 TMP_54 TMP_68 H5))))))))) in (or_ind TMP_13 TMP_20 TMP_23
+TMP_45 TMP_69 H4)))))))))))))))))))))))))) in (let TMP_141 \def (\lambda (c2:
+C).(\lambda (c3: C).(\lambda (_: (wf3 g c2 c3)).(\lambda (H1: ((\forall (c4:
+C).((wf3 g c2 c4) \to (eq C c3 c4))))).(\lambda (u: T).(\lambda (H2:
+((\forall (t: T).((ty3 g c2 u t) \to False)))).(\lambda (b: B).(\lambda (c0:
+C).(\lambda (H3: (wf3 g (CHead c2 (Bind b) u) c0)).(let H_x \def
+(wf3_gen_bind1 g c2 c0 u b H3) in (let H4 \def H_x in (let TMP_73 \def
+(\lambda (c4: C).(\lambda (_: T).(let TMP_71 \def (Bind b) in (let TMP_72
+\def (CHead c4 TMP_71 u) in (eq C c0 TMP_72))))) in (let TMP_74 \def (\lambda
+(c4: C).(\lambda (_: T).(wf3 g c2 c4))) in (let TMP_75 \def (\lambda (_:
+C).(\lambda (w: T).(ty3 g c2 u w))) in (let TMP_76 \def (ex3_2 C T TMP_73
+TMP_74 TMP_75) in (let TMP_80 \def (\lambda (c4: C).(let TMP_77 \def (Bind
+Void) in (let TMP_78 \def (TSort O) in (let TMP_79 \def (CHead c4 TMP_77
+TMP_78) in (eq C c0 TMP_79))))) in (let TMP_81 \def (\lambda (c4: C).(wf3 g
+c2 c4)) in (let TMP_82 \def (\lambda (_: C).(\forall (w: T).((ty3 g c2 u w)
+\to False))) in (let TMP_83 \def (ex3 C TMP_80 TMP_81 TMP_82) in (let TMP_84
+\def (Bind Void) in (let TMP_85 \def (TSort O) in (let TMP_86 \def (CHead c3
+TMP_84 TMP_85) in (let TMP_87 \def (eq C TMP_86 c0) in (let TMP_111 \def
+(\lambda (H5: (ex3_2 C T (\lambda (c4: C).(\lambda (_: T).(eq C c0 (CHead c4
+(Bind b) u)))) (\lambda (c4: C).(\lambda (_: T).(wf3 g c2 c4))) (\lambda (_:
+C).(\lambda (w: T).(ty3 g c2 u w))))).(let TMP_90 \def (\lambda (c4:
+C).(\lambda (_: T).(let TMP_88 \def (Bind b) in (let TMP_89 \def (CHead c4
+TMP_88 u) in (eq C c0 TMP_89))))) in (let TMP_91 \def (\lambda (c4:
+C).(\lambda (_: T).(wf3 g c2 c4))) in (let TMP_92 \def (\lambda (_:
+C).(\lambda (w: T).(ty3 g c2 u w))) in (let TMP_93 \def (Bind Void) in (let
+TMP_94 \def (TSort O) in (let TMP_95 \def (CHead c3 TMP_93 TMP_94) in (let
+TMP_96 \def (eq C TMP_95 c0) in (let TMP_110 \def (\lambda (x0: C).(\lambda
+(x1: T).(\lambda (H6: (eq C c0 (CHead x0 (Bind b) u))).(\lambda (_: (wf3 g c2
+x0)).(\lambda (H8: (ty3 g c2 u x1)).(let TMP_97 \def (Bind b) in (let TMP_98
+\def (CHead x0 TMP_97 u) in (let TMP_102 \def (\lambda (c4: C).(let TMP_99
+\def (Bind Void) in (let TMP_100 \def (TSort O) in (let TMP_101 \def (CHead
+c3 TMP_99 TMP_100) in (eq C TMP_101 c4))))) in (let H_x0 \def (H2 x1 H8) in
+(let H9 \def H_x0 in (let TMP_103 \def (Bind Void) in (let TMP_104 \def
+(TSort O) in (let TMP_105 \def (CHead c3 TMP_103 TMP_104) in (let TMP_106
+\def (Bind b) in (let TMP_107 \def (CHead x0 TMP_106 u) in (let TMP_108 \def
+(eq C TMP_105 TMP_107) in (let TMP_109 \def (False_ind TMP_108 H9) in
+(eq_ind_r C TMP_98 TMP_102 TMP_109 c0 H6)))))))))))))))))) in (ex3_2_ind C T
+TMP_90 TMP_91 TMP_92 TMP_96 TMP_110 H5)))))))))) in (let TMP_140 \def
+(\lambda (H5: (ex3 C (\lambda (c4: C).(eq C c0 (CHead c4 (Bind Void) (TSort
+O)))) (\lambda (c4: C).(wf3 g c2 c4)) (\lambda (_: C).(\forall (w: T).((ty3 g
+c2 u w) \to False))))).(let TMP_115 \def (\lambda (c4: C).(let TMP_112 \def
+(Bind Void) in (let TMP_113 \def (TSort O) in (let TMP_114 \def (CHead c4
+TMP_112 TMP_113) in (eq C c0 TMP_114))))) in (let TMP_116 \def (\lambda (c4:
+C).(wf3 g c2 c4)) in (let TMP_117 \def (\lambda (_: C).(\forall (w: T).((ty3
+g c2 u w) \to False))) in (let TMP_118 \def (Bind Void) in (let TMP_119 \def
+(TSort O) in (let TMP_120 \def (CHead c3 TMP_118 TMP_119) in (let TMP_121
+\def (eq C TMP_120 c0) in (let TMP_139 \def (\lambda (x0: C).(\lambda (H6:
+(eq C c0 (CHead x0 (Bind Void) (TSort O)))).(\lambda (H7: (wf3 g c2
+x0)).(\lambda (_: ((\forall (w: T).((ty3 g c2 u w) \to False)))).(let TMP_122
+\def (Bind Void) in (let TMP_123 \def (TSort O) in (let TMP_124 \def (CHead
+x0 TMP_122 TMP_123) in (let TMP_128 \def (\lambda (c4: C).(let TMP_125 \def
+(Bind Void) in (let TMP_126 \def (TSort O) in (let TMP_127 \def (CHead c3
+TMP_125 TMP_126) in (eq C TMP_127 c4))))) in (let TMP_129 \def (Bind Void) in
+(let TMP_130 \def (Bind Void) in (let TMP_131 \def (TSort O) in (let TMP_132
+\def (TSort O) in (let TMP_133 \def (H1 x0 H7) in (let TMP_134 \def (Bind
+Void) in (let TMP_135 \def (refl_equal K TMP_134) in (let TMP_136 \def (TSort
+O) in (let TMP_137 \def (refl_equal T TMP_136) in (let TMP_138 \def (f_equal3
+C K T C CHead c3 x0 TMP_129 TMP_130 TMP_131 TMP_132 TMP_133 TMP_135 TMP_137)
+in (eq_ind_r C TMP_124 TMP_128 TMP_138 c0 H6))))))))))))))))))) in (ex3_ind C
+TMP_115 TMP_116 TMP_117 TMP_121 TMP_139 H5)))))))))) in (or_ind TMP_76 TMP_83
+TMP_87 TMP_111 TMP_140 H4)))))))))))))))))))))))))) in (let TMP_142 \def
+(\lambda (c2: C).(\lambda (c3: C).(\lambda (_: (wf3 g c2 c3)).(\lambda (H1:
+((\forall (c4: C).((wf3 g c2 c4) \to (eq C c3 c4))))).(\lambda (u:
+T).(\lambda (f: F).(\lambda (c0: C).(\lambda (H2: (wf3 g (CHead c2 (Flat f)
+u) c0)).(let H_y \def (wf3_gen_flat1 g c2 c0 u f H2) in (H1 c0 H_y))))))))))
+in (wf3_ind g TMP_1 TMP_7 TMP_70 TMP_141 TMP_142 c c1 H))))))))).