-T).(subst0 (clen c0) t t0 t2)))).(ex3_ind T (\lambda (_: T).(eq K (Flat f)
-(Bind Abbr))) (\lambda (t0: T).(pr0 t1 t0)) (\lambda (t0: T).(subst0 (clen
-c0) t t0 t2)) (eq T t1 t2) (\lambda (x0: T).(\lambda (H5: (eq K (Flat f)
-(Bind Abbr))).(\lambda (_: (pr0 t1 x0)).(\lambda (_: (subst0 (clen c0) t x0
-t2)).(let H8 \def (eq_ind K (Flat f) (\lambda (ee: K).(match ee in K return
-(\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow
-True])) I (Bind Abbr) H5) in (False_ind (eq T t1 t2) H8)))))) H4)) H3)))))))
-k)) (\lambda (H1: (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P:
-Prop).P))) (\lambda (t2: T).(pr2 c0 t1 t2)))).(ex2_ind T (\lambda (t2:
-T).((eq T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 c0 t1 t2))
-(or (\forall (t2: T).((pr2 (CTail k t c0) t1 t2) \to (eq T t1 t2))) (ex2 T
-(\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2:
-T).(pr2 (CTail k t c0) t1 t2)))) (\lambda (x: T).(\lambda (H2: (((eq T t1 x)
-\to (\forall (P: Prop).P)))).(\lambda (H3: (pr2 c0 t1 x)).(or_intror (\forall
+T).(subst0 (clen c0) t t0 t2)) (eq T t1 t2) (\lambda (x0: T).(\lambda (H5:
+(eq K (Flat f) (Bind Abbr))).(\lambda (_: (pr0 t1 x0)).(\lambda (_: (subst0
+(clen c0) t x0 t2)).(let H8 \def (eq_ind K (Flat f) (\lambda (ee: K).(match
+ee with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])) I (Bind
+Abbr) H5) in (False_ind (eq T t1 t2) H8)))))) H4)) H3))))))) k)) (\lambda
+(H1: (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P)))
+(\lambda (t2: T).(pr2 c0 t1 t2)))).(ex2_ind T (\lambda (t2: T).((eq T t1 t2)
+\to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 c0 t1 t2)) (or (\forall