-t)).(let TMP_1 \def (\lambda (c: C).(\lambda (t0: T).(\lambda (t2:
-T).(\forall (i: nat).(\forall (u: T).(\forall (c2: C).(\forall (t3:
-T).((fsubst0 i u c t0 c2 t3) \to (\forall (e: C).((getl i c (CHead e (Bind
-Abbr) u)) \to (pc3 c2 t3 t2))))))))))) in (let TMP_47 \def (\lambda (c:
-C).(\lambda (t2: T).(\lambda (t3: T).(\lambda (H0: (pr0 t2 t3)).(\lambda (i:
-nat).(\lambda (u: T).(\lambda (c2: C).(\lambda (t0: T).(\lambda (H1: (fsubst0
-i u c t2 c2 t0)).(let TMP_2 \def (\lambda (c0: C).(\lambda (t4: T).(\forall
-(e: C).((getl i c (CHead e (Bind Abbr) u)) \to (pc3 c0 t4 t3))))) in (let
-TMP_21 \def (\lambda (t4: T).(\lambda (H2: (subst0 i u t2 t4)).(\lambda (e:
-C).(\lambda (H3: (getl i c (CHead e (Bind Abbr) u))).(let TMP_3 \def (pr0 t4
-t3) in (let TMP_4 \def (\lambda (w2: T).(pr0 t4 w2)) in (let TMP_5 \def
-(\lambda (w2: T).(subst0 i u t3 w2)) in (let TMP_6 \def (ex2 T TMP_4 TMP_5)
-in (let TMP_7 \def (pc3 c t4 t3) in (let TMP_9 \def (\lambda (H4: (pr0 t4
-t3)).(let TMP_8 \def (pr2_free c t4 t3 H4) in (pc3_pr2_r c t4 t3 TMP_8))) in
-(let TMP_18 \def (\lambda (H4: (ex2 T (\lambda (w2: T).(pr0 t4 w2)) (\lambda
-(w2: T).(subst0 i u t3 w2)))).(let TMP_10 \def (\lambda (w2: T).(pr0 t4 w2))
-in (let TMP_11 \def (\lambda (w2: T).(subst0 i u t3 w2)) in (let TMP_12 \def
-(pc3 c t4 t3) in (let TMP_17 \def (\lambda (x: T).(\lambda (H5: (pr0 t4
-x)).(\lambda (H6: (subst0 i u t3 x)).(let TMP_13 \def (pr2_free c t4 x H5) in
-(let TMP_14 \def (pr0_refl t3) in (let TMP_15 \def (pr2_delta c e u i H3 t3
-t3 TMP_14 x H6) in (let TMP_16 \def (pc3_pr2_x c x t3 TMP_15) in (pc3_pr2_u c
-x t4 TMP_13 t3 TMP_16)))))))) in (ex2_ind T TMP_10 TMP_11 TMP_12 TMP_17
-H4)))))) in (let TMP_19 \def (pr0_refl u) in (let TMP_20 \def (pr0_subst0 t2
-t3 H0 u t4 i H2 u TMP_19) in (or_ind TMP_3 TMP_6 TMP_7 TMP_9 TMP_18
-TMP_20)))))))))))))) in (let TMP_23 \def (\lambda (c0: C).(\lambda (_:
-(csubst0 i u c c0)).(\lambda (e: C).(\lambda (_: (getl i c (CHead e (Bind
-Abbr) u))).(let TMP_22 \def (pr2_free c0 t2 t3 H0) in (pc3_pr2_r c0 t2 t3
-TMP_22)))))) in (let TMP_46 \def (\lambda (t4: T).(\lambda (H2: (subst0 i u
-t2 t4)).(\lambda (c0: C).(\lambda (H3: (csubst0 i u c c0)).(\lambda (e:
-C).(\lambda (H4: (getl i c (CHead e (Bind Abbr) u))).(let TMP_24 \def (pr0 t4
-t3) in (let TMP_25 \def (\lambda (w2: T).(pr0 t4 w2)) in (let TMP_26 \def
-(\lambda (w2: T).(subst0 i u t3 w2)) in (let TMP_27 \def (ex2 T TMP_25
-TMP_26) in (let TMP_28 \def (pc3 c0 t4 t3) in (let TMP_30 \def (\lambda (H5:
-(pr0 t4 t3)).(let TMP_29 \def (pr2_free c0 t4 t3 H5) in (pc3_pr2_r c0 t4 t3
-TMP_29))) in (let TMP_43 \def (\lambda (H5: (ex2 T (\lambda (w2: T).(pr0 t4
-w2)) (\lambda (w2: T).(subst0 i u t3 w2)))).(let TMP_31 \def (\lambda (w2:
-T).(pr0 t4 w2)) in (let TMP_32 \def (\lambda (w2: T).(subst0 i u t3 w2)) in
-(let TMP_33 \def (pc3 c0 t4 t3) in (let TMP_42 \def (\lambda (x: T).(\lambda
-(H6: (pr0 t4 x)).(\lambda (H7: (subst0 i u t3 x)).(let TMP_34 \def (pr2_free
-c0 t4 x H6) in (let TMP_35 \def (le_n i) in (let TMP_36 \def (Bind Abbr) in
-(let TMP_37 \def (CHead e TMP_36 u) in (let TMP_38 \def (csubst0_getl_ge i i
-TMP_35 c c0 u H3 TMP_37 H4) in (let TMP_39 \def (pr0_refl t3) in (let TMP_40
-\def (pr2_delta c0 e u i TMP_38 t3 t3 TMP_39 x H7) in (let TMP_41 \def
-(pc3_pr2_x c0 x t3 TMP_40) in (pc3_pr2_u c0 x t4 TMP_34 t3 TMP_41))))))))))))
-in (ex2_ind T TMP_31 TMP_32 TMP_33 TMP_42 H5)))))) in (let TMP_44 \def
-(pr0_refl u) in (let TMP_45 \def (pr0_subst0 t2 t3 H0 u t4 i H2 u TMP_44) in
-(or_ind TMP_24 TMP_27 TMP_28 TMP_30 TMP_43 TMP_45)))))))))))))))) in
-(fsubst0_ind i u c t2 TMP_2 TMP_21 TMP_23 TMP_46 c2 t0 H1)))))))))))))) in
-(let TMP_549 \def (\lambda (c: C).(\lambda (d: C).(\lambda (u: T).(\lambda
-(i: nat).(\lambda (H0: (getl i c (CHead d (Bind Abbr) u))).(\lambda (t2:
-T).(\lambda (t3: T).(\lambda (H1: (pr0 t2 t3)).(\lambda (t0: T).(\lambda (H2:
-(subst0 i u t3 t0)).(\lambda (i0: nat).(\lambda (u0: T).(\lambda (c2:
-C).(\lambda (t4: T).(\lambda (H3: (fsubst0 i0 u0 c t2 c2 t4)).(let TMP_48
-\def (\lambda (c0: C).(\lambda (t5: T).(\forall (e: C).((getl i0 c (CHead e
-(Bind Abbr) u0)) \to (pc3 c0 t5 t0))))) in (let TMP_55 \def (\lambda (t5:
-T).(\lambda (H4: (subst0 i0 u0 t2 t5)).(\lambda (e: C).(\lambda (H5: (getl i0
-c (CHead e (Bind Abbr) u0))).(let TMP_49 \def (pr0_refl t2) in (let TMP_50
-\def (pr2_delta c e u0 i0 H5 t2 t2 TMP_49 t5 H4) in (let TMP_51 \def
-(pc3_pr2_r c t2 t5 TMP_50) in (let TMP_52 \def (pc3_s c t5 t2 TMP_51) in (let
-TMP_53 \def (pr2_delta c d u i H0 t2 t3 H1 t0 H2) in (let TMP_54 \def
-(pc3_pr2_r c t2 t0 TMP_53) in (pc3_t t2 c t5 TMP_52 t0 TMP_54))))))))))) in
-(let TMP_284 \def (\lambda (c0: C).(\lambda (H4: (csubst0 i0 u0 c
-c0)).(\lambda (e: C).(\lambda (H5: (getl i0 c (CHead e (Bind Abbr) u0))).(let
-TMP_56 \def (pc3 c0 t2 t0) in (let TMP_278 \def (\lambda (H6: (lt i i0)).(let
-TMP_57 \def (Bind Abbr) in (let TMP_58 \def (CHead d TMP_57 u) in (let H7
-\def (csubst0_getl_lt i0 i H6 c c0 u0 H4 TMP_58 H0) in (let TMP_59 \def (Bind
-Abbr) in (let TMP_60 \def (CHead d TMP_59 u) in (let TMP_61 \def (getl i c0
-TMP_60) in (let TMP_66 \def (\lambda (b: B).(\lambda (e0: C).(\lambda (u1:
-T).(\lambda (_: T).(let TMP_62 \def (Bind Abbr) in (let TMP_63 \def (CHead d
-TMP_62 u) in (let TMP_64 \def (Bind b) in (let TMP_65 \def (CHead e0 TMP_64
-u1) in (eq C TMP_63 TMP_65))))))))) in (let TMP_69 \def (\lambda (b:
-B).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(let TMP_67 \def (Bind b)
-in (let TMP_68 \def (CHead e0 TMP_67 w) in (getl i c0 TMP_68))))))) in (let
-TMP_72 \def (\lambda (_: B).(\lambda (_: C).(\lambda (u1: T).(\lambda (w:
-T).(let TMP_70 \def (S i) in (let TMP_71 \def (minus i0 TMP_70) in (subst0
-TMP_71 u0 u1 w))))))) in (let TMP_73 \def (ex3_4 B C T T TMP_66 TMP_69
-TMP_72) in (let TMP_78 \def (\lambda (b: B).(\lambda (e1: C).(\lambda (_:
-C).(\lambda (u1: T).(let TMP_74 \def (Bind Abbr) in (let TMP_75 \def (CHead d
-TMP_74 u) in (let TMP_76 \def (Bind b) in (let TMP_77 \def (CHead e1 TMP_76
-u1) in (eq C TMP_75 TMP_77))))))))) in (let TMP_81 \def (\lambda (b:
-B).(\lambda (_: C).(\lambda (e2: C).(\lambda (u1: T).(let TMP_79 \def (Bind
-b) in (let TMP_80 \def (CHead e2 TMP_79 u1) in (getl i c0 TMP_80))))))) in
-(let TMP_84 \def (\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda
-(_: T).(let TMP_82 \def (S i) in (let TMP_83 \def (minus i0 TMP_82) in
-(csubst0 TMP_83 u0 e1 e2))))))) in (let TMP_85 \def (ex3_4 B C C T TMP_78
-TMP_81 TMP_84) in (let TMP_90 \def (\lambda (b: B).(\lambda (e1: C).(\lambda
-(_: C).(\lambda (u1: T).(\lambda (_: T).(let TMP_86 \def (Bind Abbr) in (let
-TMP_87 \def (CHead d TMP_86 u) in (let TMP_88 \def (Bind b) in (let TMP_89
-\def (CHead e1 TMP_88 u1) in (eq C TMP_87 TMP_89)))))))))) in (let TMP_93
-\def (\lambda (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (_:
-T).(\lambda (w: T).(let TMP_91 \def (Bind b) in (let TMP_92 \def (CHead e2
-TMP_91 w) in (getl i c0 TMP_92)))))))) in (let TMP_96 \def (\lambda (_:
-B).(\lambda (_: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(let
-TMP_94 \def (S i) in (let TMP_95 \def (minus i0 TMP_94) in (subst0 TMP_95 u0
-u1 w)))))))) in (let TMP_99 \def (\lambda (_: B).(\lambda (e1: C).(\lambda
-(e2: C).(\lambda (_: T).(\lambda (_: T).(let TMP_97 \def (S i) in (let TMP_98
-\def (minus i0 TMP_97) in (csubst0 TMP_98 u0 e1 e2)))))))) in (let TMP_100
-\def (ex4_5 B C C T T TMP_90 TMP_93 TMP_96 TMP_99) in (let TMP_101 \def (pc3
-c0 t2 t0) in (let TMP_103 \def (\lambda (H8: (getl i c0 (CHead d (Bind Abbr)
-u))).(let TMP_102 \def (pr2_delta c0 d u i H8 t2 t3 H1 t0 H2) in (pc3_pr2_r
-c0 t2 t0 TMP_102))) in (let TMP_168 \def (\lambda (H8: (ex3_4 B C T T
-(\lambda (b: B).(\lambda (e0: C).(\lambda (u1: T).(\lambda (_: T).(eq C
-(CHead d (Bind Abbr) u) (CHead e0 (Bind b) u1)))))) (\lambda (b: B).(\lambda
-(e0: C).(\lambda (_: T).(\lambda (w: T).(getl i c0 (CHead e0 (Bind b) w))))))
-(\lambda (_: B).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0
-(minus i0 (S i)) u0 u1 w))))))).(let TMP_108 \def (\lambda (b: B).(\lambda
-(e0: C).(\lambda (u1: T).(\lambda (_: T).(let TMP_104 \def (Bind Abbr) in
-(let TMP_105 \def (CHead d TMP_104 u) in (let TMP_106 \def (Bind b) in (let
-TMP_107 \def (CHead e0 TMP_106 u1) in (eq C TMP_105 TMP_107))))))))) in (let
-TMP_111 \def (\lambda (b: B).(\lambda (e0: C).(\lambda (_: T).(\lambda (w:
-T).(let TMP_109 \def (Bind b) in (let TMP_110 \def (CHead e0 TMP_109 w) in
-(getl i c0 TMP_110))))))) in (let TMP_114 \def (\lambda (_: B).(\lambda (_:
-C).(\lambda (u1: T).(\lambda (w: T).(let TMP_112 \def (S i) in (let TMP_113
-\def (minus i0 TMP_112) in (subst0 TMP_113 u0 u1 w))))))) in (let TMP_115
-\def (pc3 c0 t2 t0) in (let TMP_167 \def (\lambda (x0: B).(\lambda (x1:
-C).(\lambda (x2: T).(\lambda (x3: T).(\lambda (H9: (eq C (CHead d (Bind Abbr)
-u) (CHead x1 (Bind x0) x2))).(\lambda (H10: (getl i c0 (CHead x1 (Bind x0)
-x3))).(\lambda (H11: (subst0 (minus i0 (S i)) u0 x2 x3)).(let TMP_116 \def
-(\lambda (e0: C).(match e0 with [(CSort _) \Rightarrow d | (CHead c3 _ _)
-\Rightarrow c3])) in (let TMP_117 \def (Bind Abbr) in (let TMP_118 \def
-(CHead d TMP_117 u) in (let TMP_119 \def (Bind x0) in (let TMP_120 \def
-(CHead x1 TMP_119 x2) in (let H12 \def (f_equal C C TMP_116 TMP_118 TMP_120
-H9) in (let TMP_121 \def (\lambda (e0: C).(match e0 with [(CSort _)
-\Rightarrow Abbr | (CHead _ k _) \Rightarrow (match k with [(Bind b)
-\Rightarrow b | (Flat _) \Rightarrow Abbr])])) in (let TMP_122 \def (Bind
-Abbr) in (let TMP_123 \def (CHead d TMP_122 u) in (let TMP_124 \def (Bind x0)
-in (let TMP_125 \def (CHead x1 TMP_124 x2) in (let H13 \def (f_equal C B
-TMP_121 TMP_123 TMP_125 H9) in (let TMP_126 \def (\lambda (e0: C).(match e0
-with [(CSort _) \Rightarrow u | (CHead _ _ t5) \Rightarrow t5])) in (let
-TMP_127 \def (Bind Abbr) in (let TMP_128 \def (CHead d TMP_127 u) in (let
-TMP_129 \def (Bind x0) in (let TMP_130 \def (CHead x1 TMP_129 x2) in (let H14
-\def (f_equal C T TMP_126 TMP_128 TMP_130 H9) in (let TMP_165 \def (\lambda
-(H15: (eq B Abbr x0)).(\lambda (H16: (eq C d x1)).(let TMP_133 \def (\lambda
-(t5: T).(let TMP_131 \def (S i) in (let TMP_132 \def (minus i0 TMP_131) in
-(subst0 TMP_132 u0 t5 x3)))) in (let H17 \def (eq_ind_r T x2 TMP_133 H11 u
-H14) in (let TMP_136 \def (\lambda (c3: C).(let TMP_134 \def (Bind x0) in
-(let TMP_135 \def (CHead c3 TMP_134 x3) in (getl i c0 TMP_135)))) in (let H18
-\def (eq_ind_r C x1 TMP_136 H10 d H16) in (let TMP_139 \def (\lambda (b:
-B).(let TMP_137 \def (Bind b) in (let TMP_138 \def (CHead d TMP_137 x3) in
-(getl i c0 TMP_138)))) in (let H19 \def (eq_ind_r B x0 TMP_139 H18 Abbr H15)
-in (let TMP_140 \def (\lambda (t5: T).(subst0 i x3 t3 t5)) in (let TMP_145
-\def (\lambda (t5: T).(let TMP_141 \def (S i) in (let TMP_142 \def (minus i0
-TMP_141) in (let TMP_143 \def (plus TMP_142 i) in (let TMP_144 \def (S
-TMP_143) in (subst0 TMP_144 u0 t0 t5)))))) in (let TMP_146 \def (pc3 c0 t2
-t0) in (let TMP_161 \def (\lambda (x: T).(\lambda (H20: (subst0 i x3 t3
-x)).(\lambda (H21: (subst0 (S (plus (minus i0 (S i)) i)) u0 t0 x)).(let
-TMP_147 \def (S i) in (let TMP_148 \def (minus i0 TMP_147) in (let TMP_149
-\def (plus TMP_148 i) in (let TMP_150 \def (S TMP_149) in (let TMP_151 \def
-(\lambda (n: nat).(subst0 n u0 t0 x)) in (let TMP_152 \def (lt_plus_minus_r i
-i0 H6) in (let H22 \def (eq_ind_r nat TMP_150 TMP_151 H21 i0 TMP_152) in (let
-TMP_153 \def (pr2_delta c0 d x3 i H19 t2 t3 H1 x H20) in (let TMP_154 \def
-(le_n i0) in (let TMP_155 \def (Bind Abbr) in (let TMP_156 \def (CHead e
-TMP_155 u0) in (let TMP_157 \def (csubst0_getl_ge i0 i0 TMP_154 c c0 u0 H4
-TMP_156 H5) in (let TMP_158 \def (pr0_refl t0) in (let TMP_159 \def
-(pr2_delta c0 e u0 i0 TMP_157 t0 t0 TMP_158 x H22) in (let TMP_160 \def
-(pc3_pr2_x c0 x t0 TMP_159) in (pc3_pr2_u c0 x t2 TMP_153 t0
-TMP_160))))))))))))))))))) in (let TMP_162 \def (S i) in (let TMP_163 \def
-(minus i0 TMP_162) in (let TMP_164 \def (subst0_subst0_back t3 t0 u i H2 x3
-u0 TMP_163 H17) in (ex2_ind T TMP_140 TMP_145 TMP_146 TMP_161
-TMP_164)))))))))))))))) in (let TMP_166 \def (TMP_165 H13) in (TMP_166
-H12)))))))))))))))))))))))))))) in (ex3_4_ind B C T T TMP_108 TMP_111 TMP_114
-TMP_115 TMP_167 H8))))))) in (let TMP_209 \def (\lambda (H8: (ex3_4 B C C T
-(\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(eq C
-(CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1)))))) (\lambda (b: B).(\lambda
-(_: C).(\lambda (e2: C).(\lambda (u1: T).(getl i c0 (CHead e2 (Bind b)
-u1)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
-T).(csubst0 (minus i0 (S i)) u0 e1 e2))))))).(let TMP_173 \def (\lambda (b:
-B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(let TMP_169 \def (Bind
-Abbr) in (let TMP_170 \def (CHead d TMP_169 u) in (let TMP_171 \def (Bind b)
-in (let TMP_172 \def (CHead e1 TMP_171 u1) in (eq C TMP_170 TMP_172)))))))))
-in (let TMP_176 \def (\lambda (b: B).(\lambda (_: C).(\lambda (e2:
-C).(\lambda (u1: T).(let TMP_174 \def (Bind b) in (let TMP_175 \def (CHead e2
-TMP_174 u1) in (getl i c0 TMP_175))))))) in (let TMP_179 \def (\lambda (_:
-B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(let TMP_177 \def (S i)
-in (let TMP_178 \def (minus i0 TMP_177) in (csubst0 TMP_178 u0 e1 e2)))))))
-in (let TMP_180 \def (pc3 c0 t2 t0) in (let TMP_208 \def (\lambda (x0:
-B).(\lambda (x1: C).(\lambda (x2: C).(\lambda (x3: T).(\lambda (H9: (eq C
-(CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x3))).(\lambda (H10: (getl i c0
-(CHead x2 (Bind x0) x3))).(\lambda (H11: (csubst0 (minus i0 (S i)) u0 x1
-x2)).(let TMP_181 \def (\lambda (e0: C).(match e0 with [(CSort _) \Rightarrow
-d | (CHead c3 _ _) \Rightarrow c3])) in (let TMP_182 \def (Bind Abbr) in (let
-TMP_183 \def (CHead d TMP_182 u) in (let TMP_184 \def (Bind x0) in (let
-TMP_185 \def (CHead x1 TMP_184 x3) in (let H12 \def (f_equal C C TMP_181
-TMP_183 TMP_185 H9) in (let TMP_186 \def (\lambda (e0: C).(match e0 with
+t)).(pr2_ind (\lambda (c: C).(\lambda (t0: T).(\lambda (t2: T).(\forall (i:
+nat).(\forall (u: T).(\forall (c2: C).(\forall (t3: T).((fsubst0 i u c t0 c2
+t3) \to (\forall (e: C).((getl i c (CHead e (Bind Abbr) u)) \to (pc3 c2 t3
+t2))))))))))) (\lambda (c: C).(\lambda (t2: T).(\lambda (t3: T).(\lambda (H0:
+(pr0 t2 t3)).(\lambda (i: nat).(\lambda (u: T).(\lambda (c2: C).(\lambda (t0:
+T).(\lambda (H1: (fsubst0 i u c t2 c2 t0)).(fsubst0_ind i u c t2 (\lambda
+(c0: C).(\lambda (t4: T).(\forall (e: C).((getl i c (CHead e (Bind Abbr) u))
+\to (pc3 c0 t4 t3))))) (\lambda (t4: T).(\lambda (H2: (subst0 i u t2
+t4)).(\lambda (e: C).(\lambda (H3: (getl i c (CHead e (Bind Abbr)
+u))).(or_ind (pr0 t4 t3) (ex2 T (\lambda (w2: T).(pr0 t4 w2)) (\lambda (w2:
+T).(subst0 i u t3 w2))) (pc3 c t4 t3) (\lambda (H4: (pr0 t4 t3)).(pc3_pr2_r c
+t4 t3 (pr2_free c t4 t3 H4))) (\lambda (H4: (ex2 T (\lambda (w2: T).(pr0 t4
+w2)) (\lambda (w2: T).(subst0 i u t3 w2)))).(ex2_ind T (\lambda (w2: T).(pr0
+t4 w2)) (\lambda (w2: T).(subst0 i u t3 w2)) (pc3 c t4 t3) (\lambda (x:
+T).(\lambda (H5: (pr0 t4 x)).(\lambda (H6: (subst0 i u t3 x)).(pc3_pr2_u c x
+t4 (pr2_free c t4 x H5) t3 (pc3_pr2_x c x t3 (pr2_delta c e u i H3 t3 t3
+(pr0_refl t3) x H6)))))) H4)) (pr0_subst0 t2 t3 H0 u t4 i H2 u (pr0_refl
+u))))))) (\lambda (c0: C).(\lambda (_: (csubst0 i u c c0)).(\lambda (e:
+C).(\lambda (_: (getl i c (CHead e (Bind Abbr) u))).(pc3_pr2_r c0 t2 t3
+(pr2_free c0 t2 t3 H0)))))) (\lambda (t4: T).(\lambda (H2: (subst0 i u t2
+t4)).(\lambda (c0: C).(\lambda (H3: (csubst0 i u c c0)).(\lambda (e:
+C).(\lambda (H4: (getl i c (CHead e (Bind Abbr) u))).(or_ind (pr0 t4 t3) (ex2
+T (\lambda (w2: T).(pr0 t4 w2)) (\lambda (w2: T).(subst0 i u t3 w2))) (pc3 c0
+t4 t3) (\lambda (H5: (pr0 t4 t3)).(pc3_pr2_r c0 t4 t3 (pr2_free c0 t4 t3
+H5))) (\lambda (H5: (ex2 T (\lambda (w2: T).(pr0 t4 w2)) (\lambda (w2:
+T).(subst0 i u t3 w2)))).(ex2_ind T (\lambda (w2: T).(pr0 t4 w2)) (\lambda
+(w2: T).(subst0 i u t3 w2)) (pc3 c0 t4 t3) (\lambda (x: T).(\lambda (H6: (pr0
+t4 x)).(\lambda (H7: (subst0 i u t3 x)).(pc3_pr2_u c0 x t4 (pr2_free c0 t4 x
+H6) t3 (pc3_pr2_x c0 x t3 (pr2_delta c0 e u i (csubst0_getl_ge i i (le_n i) c
+c0 u H3 (CHead e (Bind Abbr) u) H4) t3 t3 (pr0_refl t3) x H7)))))) H5))
+(pr0_subst0 t2 t3 H0 u t4 i H2 u (pr0_refl u))))))))) c2 t0 H1))))))))))
+(\lambda (c: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda
+(H0: (getl i c (CHead d (Bind Abbr) u))).(\lambda (t2: T).(\lambda (t3:
+T).(\lambda (H1: (pr0 t2 t3)).(\lambda (t0: T).(\lambda (H2: (subst0 i u t3
+t0)).(\lambda (i0: nat).(\lambda (u0: T).(\lambda (c2: C).(\lambda (t4:
+T).(\lambda (H3: (fsubst0 i0 u0 c t2 c2 t4)).(fsubst0_ind i0 u0 c t2 (\lambda
+(c0: C).(\lambda (t5: T).(\forall (e: C).((getl i0 c (CHead e (Bind Abbr)
+u0)) \to (pc3 c0 t5 t0))))) (\lambda (t5: T).(\lambda (H4: (subst0 i0 u0 t2
+t5)).(\lambda (e: C).(\lambda (H5: (getl i0 c (CHead e (Bind Abbr)
+u0))).(pc3_t t2 c t5 (pc3_s c t5 t2 (pc3_pr2_r c t2 t5 (pr2_delta c e u0 i0
+H5 t2 t2 (pr0_refl t2) t5 H4))) t0 (pc3_pr2_r c t2 t0 (pr2_delta c d u i H0
+t2 t3 H1 t0 H2))))))) (\lambda (c0: C).(\lambda (H4: (csubst0 i0 u0 c
+c0)).(\lambda (e: C).(\lambda (H5: (getl i0 c (CHead e (Bind Abbr)
+u0))).(lt_le_e i i0 (pc3 c0 t2 t0) (\lambda (H6: (lt i i0)).(let H7 \def
+(csubst0_getl_lt i0 i H6 c c0 u0 H4 (CHead d (Bind Abbr) u) H0) in (or4_ind
+(getl i c0 (CHead d (Bind Abbr) u)) (ex3_4 B C T T (\lambda (b: B).(\lambda
+(e0: C).(\lambda (u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead
+e0 (Bind b) u1)))))) (\lambda (b: B).(\lambda (e0: C).(\lambda (_:
+T).(\lambda (w: T).(getl i c0 (CHead e0 (Bind b) w)))))) (\lambda (_:
+B).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0 (minus i0 (S i))
+u0 u1 w)))))) (ex3_4 B C C T (\lambda (b: B).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u1: T).(eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1))))))
+(\lambda (b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (u1: T).(getl i c0
+(CHead e2 (Bind b) u1)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2:
+C).(\lambda (_: T).(csubst0 (minus i0 (S i)) u0 e1 e2)))))) (ex4_5 B C C T T
+(\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(\lambda
+(_: T).(eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1))))))) (\lambda
+(b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(getl
+i c0 (CHead e2 (Bind b) w))))))) (\lambda (_: B).(\lambda (_: C).(\lambda (_:
+C).(\lambda (u1: T).(\lambda (w: T).(subst0 (minus i0 (S i)) u0 u1 w))))))
+(\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
+(_: T).(csubst0 (minus i0 (S i)) u0 e1 e2))))))) (pc3 c0 t2 t0) (\lambda (H8:
+(getl i c0 (CHead d (Bind Abbr) u))).(pc3_pr2_r c0 t2 t0 (pr2_delta c0 d u i
+H8 t2 t3 H1 t0 H2))) (\lambda (H8: (ex3_4 B C T T (\lambda (b: B).(\lambda
+(e0: C).(\lambda (u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead
+e0 (Bind b) u1)))))) (\lambda (b: B).(\lambda (e0: C).(\lambda (_:
+T).(\lambda (w: T).(getl i c0 (CHead e0 (Bind b) w)))))) (\lambda (_:
+B).(\lambda (_: C).(\lambda (u1: T).(\lambda (w: T).(subst0 (minus i0 (S i))
+u0 u1 w))))))).(ex3_4_ind B C T T (\lambda (b: B).(\lambda (e0: C).(\lambda
+(u1: T).(\lambda (_: T).(eq C (CHead d (Bind Abbr) u) (CHead e0 (Bind b)
+u1)))))) (\lambda (b: B).(\lambda (e0: C).(\lambda (_: T).(\lambda (w:
+T).(getl i c0 (CHead e0 (Bind b) w)))))) (\lambda (_: B).(\lambda (_:
+C).(\lambda (u1: T).(\lambda (w: T).(subst0 (minus i0 (S i)) u0 u1 w)))))
+(pc3 c0 t2 t0) (\lambda (x0: B).(\lambda (x1: C).(\lambda (x2: T).(\lambda
+(x3: T).(\lambda (H9: (eq C (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
+x2))).(\lambda (H10: (getl i c0 (CHead x1 (Bind x0) x3))).(\lambda (H11:
+(subst0 (minus i0 (S i)) u0 x2 x3)).(let H12 \def (f_equal C C (\lambda (e0:
+C).(match e0 with [(CSort _) \Rightarrow d | (CHead c3 _ _) \Rightarrow c3]))
+(CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2) H9) in ((let H13 \def
+(f_equal C B (\lambda (e0: C).(match e0 with [(CSort _) \Rightarrow Abbr |
+(CHead _ k _) \Rightarrow (match k with [(Bind b) \Rightarrow b | (Flat _)
+\Rightarrow Abbr])])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0) x2) H9) in
+((let H14 \def (f_equal C T (\lambda (e0: C).(match e0 with [(CSort _)
+\Rightarrow u | (CHead _ _ t5) \Rightarrow t5])) (CHead d (Bind Abbr) u)
+(CHead x1 (Bind x0) x2) H9) in (\lambda (H15: (eq B Abbr x0)).(\lambda (H16:
+(eq C d x1)).(let H17 \def (eq_ind_r T x2 (\lambda (t5: T).(subst0 (minus i0
+(S i)) u0 t5 x3)) H11 u H14) in (let H18 \def (eq_ind_r C x1 (\lambda (c3:
+C).(getl i c0 (CHead c3 (Bind x0) x3))) H10 d H16) in (let H19 \def (eq_ind_r
+B x0 (\lambda (b: B).(getl i c0 (CHead d (Bind b) x3))) H18 Abbr H15) in
+(ex2_ind T (\lambda (t5: T).(subst0 i x3 t3 t5)) (\lambda (t5: T).(subst0 (S
+(plus (minus i0 (S i)) i)) u0 t0 t5)) (pc3 c0 t2 t0) (\lambda (x: T).(\lambda
+(H20: (subst0 i x3 t3 x)).(\lambda (H21: (subst0 (S (plus (minus i0 (S i))
+i)) u0 t0 x)).(let H22 \def (eq_ind_r nat (S (plus (minus i0 (S i)) i))
+(\lambda (n: nat).(subst0 n u0 t0 x)) H21 i0 (lt_plus_minus_r i i0 H6)) in
+(pc3_pr2_u c0 x t2 (pr2_delta c0 d x3 i H19 t2 t3 H1 x H20) t0 (pc3_pr2_x c0
+x t0 (pr2_delta c0 e u0 i0 (csubst0_getl_ge i0 i0 (le_n i0) c c0 u0 H4 (CHead
+e (Bind Abbr) u0) H5) t0 t0 (pr0_refl t0) x H22))))))) (subst0_subst0_back t3
+t0 u i H2 x3 u0 (minus i0 (S i)) H17)))))))) H13)) H12))))))))) H8)) (\lambda
+(H8: (ex3_4 B C C T (\lambda (b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda
+(u1: T).(eq C (CHead d (Bind Abbr) u) (CHead e1 (Bind b) u1)))))) (\lambda
+(b: B).(\lambda (_: C).(\lambda (e2: C).(\lambda (u1: T).(getl i c0 (CHead e2
+(Bind b) u1)))))) (\lambda (_: B).(\lambda (e1: C).(\lambda (e2: C).(\lambda
+(_: T).(csubst0 (minus i0 (S i)) u0 e1 e2))))))).(ex3_4_ind B C C T (\lambda
+(b: B).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(eq C (CHead d (Bind
+Abbr) u) (CHead e1 (Bind b) u1)))))) (\lambda (b: B).(\lambda (_: C).(\lambda
+(e2: C).(\lambda (u1: T).(getl i c0 (CHead e2 (Bind b) u1)))))) (\lambda (_:
+B).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (minus i0 (S
+i)) u0 e1 e2))))) (pc3 c0 t2 t0) (\lambda (x0: B).(\lambda (x1: C).(\lambda
+(x2: C).(\lambda (x3: T).(\lambda (H9: (eq C (CHead d (Bind Abbr) u) (CHead
+x1 (Bind x0) x3))).(\lambda (H10: (getl i c0 (CHead x2 (Bind x0)
+x3))).(\lambda (H11: (csubst0 (minus i0 (S i)) u0 x1 x2)).(let H12 \def
+(f_equal C C (\lambda (e0: C).(match e0 with [(CSort _) \Rightarrow d |
+(CHead c3 _ _) \Rightarrow c3])) (CHead d (Bind Abbr) u) (CHead x1 (Bind x0)
+x3) H9) in ((let H13 \def (f_equal C B (\lambda (e0: C).(match e0 with