-(H: (csubt g (CHead e1 (Bind Abst) v1) c2)).(insert_eq C (CHead e1 (Bind
-Abst) v1) (\lambda (c: C).(csubt g c c2)) (\lambda (_: C).(or (ex2 C (\lambda
-(e2: C).(eq C c2 (CHead e2 (Bind Abst) v1))) (\lambda (e2: C).(csubt g e1
-e2))) (ex4_2 C T (\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind
-Abbr) v2)))) (\lambda (e2: C).(\lambda (_: T).(csubt g e1 e2))) (\lambda (_:
-C).(\lambda (v2: T).(ty3 g e1 v2 v1))) (\lambda (e2: C).(\lambda (v2: T).(ty3
-g e2 v2 v1)))))) (\lambda (y: C).(\lambda (H0: (csubt g y c2)).(csubt_ind g
-(\lambda (c: C).(\lambda (c0: C).((eq C c (CHead e1 (Bind Abst) v1)) \to (or
-(ex2 C (\lambda (e2: C).(eq C c0 (CHead e2 (Bind Abst) v1))) (\lambda (e2:
-C).(csubt g e1 e2))) (ex4_2 C T (\lambda (e2: C).(\lambda (v2: T).(eq C c0
-(CHead e2 (Bind Abbr) v2)))) (\lambda (e2: C).(\lambda (_: T).(csubt g e1
-e2))) (\lambda (_: C).(\lambda (v2: T).(ty3 g e1 v2 v1))) (\lambda (e2:
-C).(\lambda (v2: T).(ty3 g e2 v2 v1)))))))) (\lambda (n: nat).(\lambda (H1:
-(eq C (CSort n) (CHead e1 (Bind Abst) v1))).(let H2 \def (eq_ind C (CSort n)
-(\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _)
-\Rightarrow True | (CHead _ _ _) \Rightarrow False])) I (CHead e1 (Bind Abst)
-v1) H1) in (False_ind (or (ex2 C (\lambda (e2: C).(eq C (CSort n) (CHead e2
-(Bind Abst) v1))) (\lambda (e2: C).(csubt g e1 e2))) (ex4_2 C T (\lambda (e2:
-C).(\lambda (v2: T).(eq C (CSort n) (CHead e2 (Bind Abbr) v2)))) (\lambda
-(e2: C).(\lambda (_: T).(csubt g e1 e2))) (\lambda (_: C).(\lambda (v2:
-T).(ty3 g e1 v2 v1))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2 v1)))))
-H2)))) (\lambda (c1: C).(\lambda (c3: C).(\lambda (H1: (csubt g c1
-c3)).(\lambda (H2: (((eq C c1 (CHead e1 (Bind Abst) v1)) \to (or (ex2 C
+(H: (csubt g (CHead e1 (Bind Abst) v1) c2)).(let TMP_1 \def (Bind Abst) in
+(let TMP_2 \def (CHead e1 TMP_1 v1) in (let TMP_3 \def (\lambda (c: C).(csubt
+g c c2)) in (let TMP_16 \def (\lambda (_: C).(let TMP_6 \def (\lambda (e2:
+C).(let TMP_4 \def (Bind Abst) in (let TMP_5 \def (CHead e2 TMP_4 v1) in (eq
+C c2 TMP_5)))) in (let TMP_7 \def (\lambda (e2: C).(csubt g e1 e2)) in (let
+TMP_8 \def (ex2 C TMP_6 TMP_7) in (let TMP_11 \def (\lambda (e2: C).(\lambda
+(v2: T).(let TMP_9 \def (Bind Abbr) in (let TMP_10 \def (CHead e2 TMP_9 v2)
+in (eq C c2 TMP_10))))) in (let TMP_12 \def (\lambda (e2: C).(\lambda (_:
+T).(csubt g e1 e2))) in (let TMP_13 \def (\lambda (_: C).(\lambda (v2:
+T).(ty3 g e1 v2 v1))) in (let TMP_14 \def (\lambda (e2: C).(\lambda (v2:
+T).(ty3 g e2 v2 v1))) in (let TMP_15 \def (ex4_2 C T TMP_11 TMP_12 TMP_13
+TMP_14) in (or TMP_8 TMP_15)))))))))) in (let TMP_218 \def (\lambda (y:
+C).(\lambda (H0: (csubt g y c2)).(let TMP_29 \def (\lambda (c: C).(\lambda
+(c0: C).((eq C c (CHead e1 (Bind Abst) v1)) \to (let TMP_19 \def (\lambda
+(e2: C).(let TMP_17 \def (Bind Abst) in (let TMP_18 \def (CHead e2 TMP_17 v1)
+in (eq C c0 TMP_18)))) in (let TMP_20 \def (\lambda (e2: C).(csubt g e1 e2))
+in (let TMP_21 \def (ex2 C TMP_19 TMP_20) in (let TMP_24 \def (\lambda (e2:
+C).(\lambda (v2: T).(let TMP_22 \def (Bind Abbr) in (let TMP_23 \def (CHead
+e2 TMP_22 v2) in (eq C c0 TMP_23))))) in (let TMP_25 \def (\lambda (e2:
+C).(\lambda (_: T).(csubt g e1 e2))) in (let TMP_26 \def (\lambda (_:
+C).(\lambda (v2: T).(ty3 g e1 v2 v1))) in (let TMP_27 \def (\lambda (e2:
+C).(\lambda (v2: T).(ty3 g e2 v2 v1))) in (let TMP_28 \def (ex4_2 C T TMP_24
+TMP_25 TMP_26 TMP_27) in (or TMP_21 TMP_28)))))))))))) in (let TMP_49 \def
+(\lambda (n: nat).(\lambda (H1: (eq C (CSort n) (CHead e1 (Bind Abst)
+v1))).(let TMP_30 \def (CSort n) in (let TMP_31 \def (\lambda (ee: C).(match
+ee with [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow False])) in
+(let TMP_32 \def (Bind Abst) in (let TMP_33 \def (CHead e1 TMP_32 v1) in (let
+H2 \def (eq_ind C TMP_30 TMP_31 I TMP_33 H1) in (let TMP_37 \def (\lambda
+(e2: C).(let TMP_34 \def (CSort n) in (let TMP_35 \def (Bind Abst) in (let
+TMP_36 \def (CHead e2 TMP_35 v1) in (eq C TMP_34 TMP_36))))) in (let TMP_38
+\def (\lambda (e2: C).(csubt g e1 e2)) in (let TMP_39 \def (ex2 C TMP_37
+TMP_38) in (let TMP_43 \def (\lambda (e2: C).(\lambda (v2: T).(let TMP_40
+\def (CSort n) in (let TMP_41 \def (Bind Abbr) in (let TMP_42 \def (CHead e2
+TMP_41 v2) in (eq C TMP_40 TMP_42)))))) in (let TMP_44 \def (\lambda (e2:
+C).(\lambda (_: T).(csubt g e1 e2))) in (let TMP_45 \def (\lambda (_:
+C).(\lambda (v2: T).(ty3 g e1 v2 v1))) in (let TMP_46 \def (\lambda (e2:
+C).(\lambda (v2: T).(ty3 g e2 v2 v1))) in (let TMP_47 \def (ex4_2 C T TMP_43
+TMP_44 TMP_45 TMP_46) in (let TMP_48 \def (or TMP_39 TMP_47) in (False_ind
+TMP_48 H2))))))))))))))))) in (let TMP_137 \def (\lambda (c1: C).(\lambda
+(c3: C).(\lambda (H1: (csubt g c1 c3)).(\lambda (H2: (((eq C c1 (CHead e1
+(Bind Abst) v1)) \to (or (ex2 C (\lambda (e2: C).(eq C c3 (CHead e2 (Bind
+Abst) v1))) (\lambda (e2: C).(csubt g e1 e2))) (ex4_2 C T (\lambda (e2:
+C).(\lambda (v2: T).(eq C c3 (CHead e2 (Bind Abbr) v2)))) (\lambda (e2:
+C).(\lambda (_: T).(csubt g e1 e2))) (\lambda (_: C).(\lambda (v2: T).(ty3 g
+e1 v2 v1))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2
+v1)))))))).(\lambda (k: K).(\lambda (u: T).(\lambda (H3: (eq C (CHead c1 k u)
+(CHead e1 (Bind Abst) v1))).(let TMP_50 \def (\lambda (e: C).(match e with
+[(CSort _) \Rightarrow c1 | (CHead c _ _) \Rightarrow c])) in (let TMP_51
+\def (CHead c1 k u) in (let TMP_52 \def (Bind Abst) in (let TMP_53 \def
+(CHead e1 TMP_52 v1) in (let H4 \def (f_equal C C TMP_50 TMP_51 TMP_53 H3) in
+(let TMP_54 \def (\lambda (e: C).(match e with [(CSort _) \Rightarrow k |
+(CHead _ k0 _) \Rightarrow k0])) in (let TMP_55 \def (CHead c1 k u) in (let
+TMP_56 \def (Bind Abst) in (let TMP_57 \def (CHead e1 TMP_56 v1) in (let H5
+\def (f_equal C K TMP_54 TMP_55 TMP_57 H3) in (let TMP_58 \def (\lambda (e:
+C).(match e with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t])) in
+(let TMP_59 \def (CHead c1 k u) in (let TMP_60 \def (Bind Abst) in (let
+TMP_61 \def (CHead e1 TMP_60 v1) in (let H6 \def (f_equal C T TMP_58 TMP_59
+TMP_61 H3) in (let TMP_135 \def (\lambda (H7: (eq K k (Bind Abst))).(\lambda
+(H8: (eq C c1 e1)).(let TMP_76 \def (\lambda (t: T).(let TMP_65 \def (\lambda
+(e2: C).(let TMP_62 \def (CHead c3 k t) in (let TMP_63 \def (Bind Abst) in
+(let TMP_64 \def (CHead e2 TMP_63 v1) in (eq C TMP_62 TMP_64))))) in (let
+TMP_66 \def (\lambda (e2: C).(csubt g e1 e2)) in (let TMP_67 \def (ex2 C
+TMP_65 TMP_66) in (let TMP_71 \def (\lambda (e2: C).(\lambda (v2: T).(let
+TMP_68 \def (CHead c3 k t) in (let TMP_69 \def (Bind Abbr) in (let TMP_70
+\def (CHead e2 TMP_69 v2) in (eq C TMP_68 TMP_70)))))) in (let TMP_72 \def
+(\lambda (e2: C).(\lambda (_: T).(csubt g e1 e2))) in (let TMP_73 \def
+(\lambda (_: C).(\lambda (v2: T).(ty3 g e1 v2 v1))) in (let TMP_74 \def
+(\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2 v1))) in (let TMP_75 \def
+(ex4_2 C T TMP_71 TMP_72 TMP_73 TMP_74) in (or TMP_67 TMP_75)))))))))) in
+(let TMP_77 \def (Bind Abst) in (let TMP_92 \def (\lambda (k0: K).(let TMP_81
+\def (\lambda (e2: C).(let TMP_78 \def (CHead c3 k0 v1) in (let TMP_79 \def
+(Bind Abst) in (let TMP_80 \def (CHead e2 TMP_79 v1) in (eq C TMP_78
+TMP_80))))) in (let TMP_82 \def (\lambda (e2: C).(csubt g e1 e2)) in (let
+TMP_83 \def (ex2 C TMP_81 TMP_82) in (let TMP_87 \def (\lambda (e2:
+C).(\lambda (v2: T).(let TMP_84 \def (CHead c3 k0 v1) in (let TMP_85 \def
+(Bind Abbr) in (let TMP_86 \def (CHead e2 TMP_85 v2) in (eq C TMP_84
+TMP_86)))))) in (let TMP_88 \def (\lambda (e2: C).(\lambda (_: T).(csubt g e1
+e2))) in (let TMP_89 \def (\lambda (_: C).(\lambda (v2: T).(ty3 g e1 v2 v1)))
+in (let TMP_90 \def (\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2 v1))) in
+(let TMP_91 \def (ex4_2 C T TMP_87 TMP_88 TMP_89 TMP_90) in (or TMP_83
+TMP_91)))))))))) in (let TMP_105 \def (\lambda (c: C).((eq C c (CHead e1
+(Bind Abst) v1)) \to (let TMP_95 \def (\lambda (e2: C).(let TMP_93 \def (Bind
+Abst) in (let TMP_94 \def (CHead e2 TMP_93 v1) in (eq C c3 TMP_94)))) in (let
+TMP_96 \def (\lambda (e2: C).(csubt g e1 e2)) in (let TMP_97 \def (ex2 C
+TMP_95 TMP_96) in (let TMP_100 \def (\lambda (e2: C).(\lambda (v2: T).(let
+TMP_98 \def (Bind Abbr) in (let TMP_99 \def (CHead e2 TMP_98 v2) in (eq C c3
+TMP_99))))) in (let TMP_101 \def (\lambda (e2: C).(\lambda (_: T).(csubt g e1
+e2))) in (let TMP_102 \def (\lambda (_: C).(\lambda (v2: T).(ty3 g e1 v2
+v1))) in (let TMP_103 \def (\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2
+v1))) in (let TMP_104 \def (ex4_2 C T TMP_100 TMP_101 TMP_102 TMP_103) in (or
+TMP_97 TMP_104))))))))))) in (let H9 \def (eq_ind C c1 TMP_105 H2 e1 H8) in
+(let TMP_106 \def (\lambda (c: C).(csubt g c c3)) in (let H10 \def (eq_ind C
+c1 TMP_106 H1 e1 H8) in (let TMP_111 \def (\lambda (e2: C).(let TMP_107 \def
+(Bind Abst) in (let TMP_108 \def (CHead c3 TMP_107 v1) in (let TMP_109 \def
+(Bind Abst) in (let TMP_110 \def (CHead e2 TMP_109 v1) in (eq C TMP_108
+TMP_110)))))) in (let TMP_112 \def (\lambda (e2: C).(csubt g e1 e2)) in (let
+TMP_113 \def (ex2 C TMP_111 TMP_112) in (let TMP_118 \def (\lambda (e2:
+C).(\lambda (v2: T).(let TMP_114 \def (Bind Abst) in (let TMP_115 \def (CHead
+c3 TMP_114 v1) in (let TMP_116 \def (Bind Abbr) in (let TMP_117 \def (CHead
+e2 TMP_116 v2) in (eq C TMP_115 TMP_117))))))) in (let TMP_119 \def (\lambda
+(e2: C).(\lambda (_: T).(csubt g e1 e2))) in (let TMP_120 \def (\lambda (_:
+C).(\lambda (v2: T).(ty3 g e1 v2 v1))) in (let TMP_121 \def (\lambda (e2:
+C).(\lambda (v2: T).(ty3 g e2 v2 v1))) in (let TMP_122 \def (ex4_2 C T
+TMP_118 TMP_119 TMP_120 TMP_121) in (let TMP_127 \def (\lambda (e2: C).(let
+TMP_123 \def (Bind Abst) in (let TMP_124 \def (CHead c3 TMP_123 v1) in (let
+TMP_125 \def (Bind Abst) in (let TMP_126 \def (CHead e2 TMP_125 v1) in (eq C
+TMP_124 TMP_126)))))) in (let TMP_128 \def (\lambda (e2: C).(csubt g e1 e2))
+in (let TMP_129 \def (Bind Abst) in (let TMP_130 \def (CHead c3 TMP_129 v1)
+in (let TMP_131 \def (refl_equal C TMP_130) in (let TMP_132 \def (ex_intro2 C
+TMP_127 TMP_128 c3 TMP_131 H10) in (let TMP_133 \def (or_introl TMP_113
+TMP_122 TMP_132) in (let TMP_134 \def (eq_ind_r K TMP_77 TMP_92 TMP_133 k H7)
+in (eq_ind_r T v1 TMP_76 TMP_134 u H6)))))))))))))))))))))))))) in (let
+TMP_136 \def (TMP_135 H5) in (TMP_136 H4))))))))))))))))))))))))) in (let
+TMP_160 \def (\lambda (c1: C).(\lambda (c3: C).(\lambda (_: (csubt g c1
+c3)).(\lambda (_: (((eq C c1 (CHead e1 (Bind Abst) v1)) \to (or (ex2 C