-(t3: T).(pr0 z1 t3))))))) (eq T (THead (Flat Appl) t t0) t2) (\lambda (x0:
-B).(\lambda (x1: T).(\lambda (x2: T).(\lambda (x3: T).(\lambda (x4:
-T).(\lambda (x5: T).(\lambda (_: (not (eq B x0 Abst))).(\lambda (H10: (eq T
-t0 (THead (Bind x0) x1 x2))).(\lambda (H11: (eq T t2 (THead (Bind x0) x4
-(THead (Flat Appl) (lift (S O) O x3) x5)))).(\lambda (_: (pr0 t x3)).(\lambda
-(_: (pr0 x1 x4)).(\lambda (_: (pr0 x2 x5)).(eq_ind_r T (THead (Bind x0) x4
-(THead (Flat Appl) (lift (S O) O x3) x5)) (\lambda (t3: T).(eq T (THead (Flat
-Appl) t t0) t3)) (let H15 \def (eq_ind T t0 (\lambda (t3: T).(\forall (t4:
-T).((pr0 t3 t4) \to (eq T t3 t4)))) H6 (THead (Bind x0) x1 x2) H10) in (let
-H16 \def (eq_ind T t0 (\lambda (t3: T).(\forall (b: B).(\forall (w:
-T).(\forall (u: T).((eq T t3 (THead (Bind b) w u)) \to (\forall (P:
-Prop).P)))))) H2 (THead (Bind x0) x1 x2) H10) in (eq_ind_r T (THead (Bind x0)
-x1 x2) (\lambda (t3: T).(eq T (THead (Flat Appl) t t3) (THead (Bind x0) x4
-(THead (Flat Appl) (lift (S O) O x3) x5)))) (H16 x0 x1 x2 (H15 (THead (Bind
-x0) x1 x2) (pr0_refl (THead (Bind x0) x1 x2))) (eq T (THead (Flat Appl) t
-(THead (Bind x0) x1 x2)) (THead (Bind x0) x4 (THead (Flat Appl) (lift (S O) O
-x3) x5)))) t0 H10))) t2 H11))))))))))))) H8)) (pr0_gen_appl t t0 t2 H7))))))
-(\lambda (H6: (ex2 T (\lambda (t2: T).((eq T t0 t2) \to (\forall (P:
-Prop).P))) (\lambda (t2: T).(pr0 t0 t2)))).(ex2_ind T (\lambda (t2: T).((eq T
-t0 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 t0 t2)) (or (\forall
-(t2: T).((pr0 (THead (Flat Appl) t t0) t2) \to (eq T (THead (Flat Appl) t t0)
-t2))) (ex2 T (\lambda (t2: T).((eq T (THead (Flat Appl) t t0) t2) \to
-(\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead (Flat Appl) t t0) t2))))
-(\lambda (x: T).(\lambda (H7: (((eq T t0 x) \to (\forall (P:
-Prop).P)))).(\lambda (H8: (pr0 t0 x)).(or_intror (\forall (t2: T).((pr0
-(THead (Flat Appl) t t0) t2) \to (eq T (THead (Flat Appl) t t0) t2))) (ex2 T
-(\lambda (t2: T).((eq T (THead (Flat Appl) t t0) t2) \to (\forall (P:
-Prop).P))) (\lambda (t2: T).(pr0 (THead (Flat Appl) t t0) t2))) (ex_intro2 T
-(\lambda (t2: T).((eq T (THead (Flat Appl) t t0) t2) \to (\forall (P:
-Prop).P))) (\lambda (t2: T).(pr0 (THead (Flat Appl) t t0) t2)) (THead (Flat
-Appl) t x) (\lambda (H9: (eq T (THead (Flat Appl) t t0) (THead (Flat Appl) t
-x))).(\lambda (P: Prop).(let H10 \def (f_equal T T (\lambda (e: T).(match e
-in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t0 | (TLRef _)
-\Rightarrow t0 | (THead _ _ t2) \Rightarrow t2])) (THead (Flat Appl) t t0)
-(THead (Flat Appl) t x) H9) in (let H11 \def (eq_ind_r T x (\lambda (t2:
-T).(pr0 t0 t2)) H8 t0 H10) in (let H12 \def (eq_ind_r T x (\lambda (t2:
-T).((eq T t0 t2) \to (\forall (P0: Prop).P0))) H7 t0 H10) in (H12 (refl_equal
-T t0) P)))))) (pr0_comp t t (pr0_refl t) t0 x H8 (Flat Appl))))))) H6)) H5)))
-(\lambda (H4: (ex2 T (\lambda (t2: T).((eq T t t2) \to (\forall (P:
-Prop).P))) (\lambda (t2: T).(pr0 t t2)))).(ex2_ind T (\lambda (t2: T).((eq T
-t t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 t t2)) (or (\forall
-(t2: T).((pr0 (THead (Flat Appl) t t0) t2) \to (eq T (THead (Flat Appl) t t0)
-t2))) (ex2 T (\lambda (t2: T).((eq T (THead (Flat Appl) t t0) t2) \to
-(\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead (Flat Appl) t t0) t2))))
-(\lambda (x: T).(\lambda (H5: (((eq T t x) \to (\forall (P:
+(t3: T).(pr0 z1 t3)))))))) (eq T (THead (Flat Appl) t t0) t2) (\lambda (H8:
+(ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2
+t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 t u2))) (\lambda (_: T).(\lambda
+(t3: T).(pr0 t0 t3))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t3: T).(eq
+T t2 (THead (Flat Appl) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 t
+u2))) (\lambda (_: T).(\lambda (t3: T).(pr0 t0 t3))) (eq T (THead (Flat Appl)
+t t0) t2) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H9: (eq T t2 (THead
+(Flat Appl) x0 x1))).(\lambda (H10: (pr0 t x0)).(\lambda (H11: (pr0 t0
+x1)).(let H_y \def (H6 x1 H11) in (let H_y0 \def (H4 x0 H10) in (let H12 \def
+(eq_ind_r T x1 (\lambda (t3: T).(pr0 t0 t3)) H11 t0 H_y) in (let H13 \def
+(eq_ind_r T x1 (\lambda (t3: T).(eq T t2 (THead (Flat Appl) x0 t3))) H9 t0
+H_y) in (let H14 \def (eq_ind_r T x0 (\lambda (t3: T).(pr0 t t3)) H10 t H_y0)
+in (let H15 \def (eq_ind_r T x0 (\lambda (t3: T).(eq T t2 (THead (Flat Appl)
+t3 t0))) H13 t H_y0) in (eq_ind_r T (THead (Flat Appl) t t0) (\lambda (t3:
+T).(eq T (THead (Flat Appl) t t0) t3)) (refl_equal T (THead (Flat Appl) t
+t0)) t2 H15)))))))))))) H8)) (\lambda (H8: (ex4_4 T T T T (\lambda (y1:
+T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t0 (THead (Bind
+Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
+(t3: T).(eq T t2 (THead (Bind Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_:
+T).(\lambda (u2: T).(\lambda (_: T).(pr0 t u2))))) (\lambda (_: T).(\lambda
+(z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3))))))).(ex4_4_ind T T T T
+(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t0
+(THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
+T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3)))))) (\lambda (_:
+T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr0 t u2))))) (\lambda
+(_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3))))) (eq
+T (THead (Flat Appl) t t0) t2) (\lambda (x0: T).(\lambda (x1: T).(\lambda
+(x2: T).(\lambda (x3: T).(\lambda (H9: (eq T t0 (THead (Bind Abst) x0
+x1))).(\lambda (H10: (eq T t2 (THead (Bind Abbr) x2 x3))).(\lambda (_: (pr0 t
+x2)).(\lambda (_: (pr0 x1 x3)).(eq_ind_r T (THead (Bind Abbr) x2 x3) (\lambda
+(t3: T).(eq T (THead (Flat Appl) t t0) t3)) (let H13 \def (eq_ind T t0
+(\lambda (t3: T).(\forall (t4: T).((pr0 t3 t4) \to (eq T t3 t4)))) H6 (THead
+(Bind Abst) x0 x1) H9) in (let H14 \def (eq_ind T t0 (\lambda (t3:
+T).(\forall (b: B).(\forall (w: T).(\forall (u: T).((eq T t3 (THead (Bind b)
+w u)) \to (\forall (P: Prop).P)))))) H2 (THead (Bind Abst) x0 x1) H9) in
+(eq_ind_r T (THead (Bind Abst) x0 x1) (\lambda (t3: T).(eq T (THead (Flat
+Appl) t t3) (THead (Bind Abbr) x2 x3))) (H14 Abst x0 x1 (H13 (THead (Bind
+Abst) x0 x1) (pr0_refl (THead (Bind Abst) x0 x1))) (eq T (THead (Flat Appl) t
+(THead (Bind Abst) x0 x1)) (THead (Bind Abbr) x2 x3))) t0 H9))) t2
+H10))))))))) H8)) (\lambda (H8: (ex6_6 B T T T T T (\lambda (b: B).(\lambda
+(_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not
+(eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda (z1:
+T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t0 (THead (Bind b)
+y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2:
+T).(\lambda (v2: T).(\lambda (t3: T).(eq T t2 (THead (Bind b) v2 (THead (Flat
+Appl) (lift (S O) O u2) t3))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda
+(_: T).(\lambda (u2: T).(\lambda (_: T).(\lambda (_: T).(pr0 t u2)))))))
+(\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
+(v2: T).(\lambda (_: T).(pr0 y1 v2))))))) (\lambda (_: B).(\lambda (_:
+T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1
+t3))))))))).(ex6_6_ind B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda
+(_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b
+Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
+T).(\lambda (_: T).(\lambda (_: T).(eq T t0 (THead (Bind b) y1 z1))))))))
+(\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
+(v2: T).(\lambda (t3: T).(eq T t2 (THead (Bind b) v2 (THead (Flat Appl) (lift
+(S O) O u2) t3))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_:
+T).(\lambda (u2: T).(\lambda (_: T).(\lambda (_: T).(pr0 t u2))))))) (\lambda
+(_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (v2:
+T).(\lambda (_: T).(pr0 y1 v2))))))) (\lambda (_: B).(\lambda (_: T).(\lambda
+(z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3)))))))
+(eq T (THead (Flat Appl) t t0) t2) (\lambda (x0: B).(\lambda (x1: T).(\lambda
+(x2: T).(\lambda (x3: T).(\lambda (x4: T).(\lambda (x5: T).(\lambda (_: (not
+(eq B x0 Abst))).(\lambda (H10: (eq T t0 (THead (Bind x0) x1 x2))).(\lambda
+(H11: (eq T t2 (THead (Bind x0) x4 (THead (Flat Appl) (lift (S O) O x3)
+x5)))).(\lambda (_: (pr0 t x3)).(\lambda (_: (pr0 x1 x4)).(\lambda (_: (pr0
+x2 x5)).(eq_ind_r T (THead (Bind x0) x4 (THead (Flat Appl) (lift (S O) O x3)
+x5)) (\lambda (t3: T).(eq T (THead (Flat Appl) t t0) t3)) (let H15 \def
+(eq_ind T t0 (\lambda (t3: T).(\forall (t4: T).((pr0 t3 t4) \to (eq T t3
+t4)))) H6 (THead (Bind x0) x1 x2) H10) in (let H16 \def (eq_ind T t0 (\lambda
+(t3: T).(\forall (b: B).(\forall (w: T).(\forall (u: T).((eq T t3 (THead
+(Bind b) w u)) \to (\forall (P: Prop).P)))))) H2 (THead (Bind x0) x1 x2) H10)
+in (eq_ind_r T (THead (Bind x0) x1 x2) (\lambda (t3: T).(eq T (THead (Flat
+Appl) t t3) (THead (Bind x0) x4 (THead (Flat Appl) (lift (S O) O x3) x5))))
+(H16 x0 x1 x2 (H15 (THead (Bind x0) x1 x2) (pr0_refl (THead (Bind x0) x1
+x2))) (eq T (THead (Flat Appl) t (THead (Bind x0) x1 x2)) (THead (Bind x0) x4
+(THead (Flat Appl) (lift (S O) O x3) x5)))) t0 H10))) t2 H11)))))))))))))
+H8)) (pr0_gen_appl t t0 t2 H7)))))) (\lambda (H6: (ex2 T (\lambda (t2:
+T).((eq T t0 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 t0
+t2)))).(ex2_ind T (\lambda (t2: T).((eq T t0 t2) \to (\forall (P: Prop).P)))
+(\lambda (t2: T).(pr0 t0 t2)) (or (\forall (t2: T).((pr0 (THead (Flat Appl) t
+t0) t2) \to (eq T (THead (Flat Appl) t t0) t2))) (ex2 T (\lambda (t2: T).((eq
+T (THead (Flat Appl) t t0) t2) \to (\forall (P: Prop).P))) (\lambda (t2:
+T).(pr0 (THead (Flat Appl) t t0) t2)))) (\lambda (x: T).(\lambda (H7: (((eq T
+t0 x) \to (\forall (P: Prop).P)))).(\lambda (H8: (pr0 t0 x)).(or_intror
+(\forall (t2: T).((pr0 (THead (Flat Appl) t t0) t2) \to (eq T (THead (Flat
+Appl) t t0) t2))) (ex2 T (\lambda (t2: T).((eq T (THead (Flat Appl) t t0) t2)
+\to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead (Flat Appl) t t0)
+t2))) (ex_intro2 T (\lambda (t2: T).((eq T (THead (Flat Appl) t t0) t2) \to
+(\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead (Flat Appl) t t0) t2))
+(THead (Flat Appl) t x) (\lambda (H9: (eq T (THead (Flat Appl) t t0) (THead
+(Flat Appl) t x))).(\lambda (P: Prop).(let H10 \def (f_equal T T (\lambda (e:
+T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t0 |
+(TLRef _) \Rightarrow t0 | (THead _ _ t2) \Rightarrow t2])) (THead (Flat
+Appl) t t0) (THead (Flat Appl) t x) H9) in (let H11 \def (eq_ind_r T x
+(\lambda (t2: T).(pr0 t0 t2)) H8 t0 H10) in (let H12 \def (eq_ind_r T x
+(\lambda (t2: T).((eq T t0 t2) \to (\forall (P0: Prop).P0))) H7 t0 H10) in
+(H12 (refl_equal T t0) P)))))) (pr0_comp t t (pr0_refl t) t0 x H8 (Flat
+Appl))))))) H6)) H5))) (\lambda (H4: (ex2 T (\lambda (t2: T).((eq T t t2) \to
+(\forall (P: Prop).P))) (\lambda (t2: T).(pr0 t t2)))).(ex2_ind T (\lambda
+(t2: T).((eq T t t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 t t2))
+(or (\forall (t2: T).((pr0 (THead (Flat Appl) t t0) t2) \to (eq T (THead
+(Flat Appl) t t0) t2))) (ex2 T (\lambda (t2: T).((eq T (THead (Flat Appl) t
+t0) t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead (Flat Appl)
+t t0) t2)))) (\lambda (x: T).(\lambda (H5: (((eq T t x) \to (\forall (P: