+\def
+ \lambda (u1: T).(\lambda (t1: T).(\lambda (x: T).(\lambda (H: (pr0 (THead
+(Flat Appl) u1 t1) x)).(pr0_inv_coq (THead (Flat Appl) u1 t1) x (\lambda (_:
+T).(\lambda (t0: T).(or3 (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T
+t0 (THead (Flat Appl) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1
+u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (ex4_4 T T T T (\lambda
+(y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead
+(Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
+T).(\lambda (t2: T).(eq T t0 (THead (Bind Abbr) u2 t2)))))) (\lambda (_:
+T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))))) (\lambda
+(_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1 t2))))))
+(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 t1 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_:
+T).(\lambda (_: T).(\lambda (u2: T).(\lambda (v2: T).(\lambda (t2: T).(eq T
+t0 (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u2) t2)))))))))
+(\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_:
+T).(\lambda (_: T).(pr0 u1 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 (t2: T).(pr0 z1 t2))))))))))) (\lambda (H0: (pr0
+(THead (Flat Appl) u1 t1) x)).(\lambda (t: T).(\lambda (H1: (eq T t (THead
+(Flat Appl) u1 t1))).(\lambda (H2: (eq T t x)).(let H3 \def (eq_ind T t
+(\lambda (t0: T).(eq T t0 (THead (Flat Appl) u1 t1))) H1 x H2) in (let H4
+\def (eq_ind T x (\lambda (t0: T).(pr0 (THead (Flat Appl) u1 t1) t0)) H0
+(THead (Flat Appl) u1 t1) H3) in (let H5 \def (eq_ind T x (\lambda (t0:
+T).(pr0 (THead (Flat Appl) u1 t1) t0)) H (THead (Flat Appl) u1 t1) H3) in
+(eq_ind_r T (THead (Flat Appl) u1 t1) (\lambda (t0: T).(or3 (ex3_2 T T
+(\lambda (u2: T).(\lambda (t2: T).(eq T t0 (THead (Flat Appl) u2 t2))))
+(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2:
+T).(pr0 t1 t2)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda
+(_: T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1 z1)))))) (\lambda (_:
+T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t2: T).(eq T t0 (THead (Bind
+Abbr) u2 t2)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
+(_: T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
+T).(\lambda (t2: T).(pr0 z1 t2)))))) (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 t1 (THead (Bind
+b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
+(u2: T).(\lambda (v2: T).(\lambda (t2: T).(eq T t0 (THead (Bind b) v2 (THead
+(Flat Appl) (lift (S O) O u2) t2))))))))) (\lambda (_: B).(\lambda (_:
+T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1
+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
+(t2: T).(pr0 z1 t2)))))))))) (or3_intro0 (ex3_2 T T (\lambda (u2: T).(\lambda
+(t2: T).(eq T (THead (Flat Appl) u1 t1) (THead (Flat Appl) u2 t2)))) (\lambda
+(u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0
+t1 t2)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
+T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1 z1)))))) (\lambda (_:
+T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t2: T).(eq T (THead (Flat Appl)
+u1 t1) (THead (Bind Abbr) u2 t2)))))) (\lambda (_: T).(\lambda (_:
+T).(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda
+(z1: T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1 t2)))))) (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 t1
+(THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
+T).(\lambda (u2: T).(\lambda (v2: T).(\lambda (t2: T).(eq T (THead (Flat
+Appl) u1 t1) (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u2)
+t2))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2:
+T).(\lambda (_: T).(\lambda (_: T).(pr0 u1 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 (t2: T).(pr0 z1 t2)))))))) (ex3_2_intro T T
+(\lambda (u2: T).(\lambda (t2: T).(eq T (THead (Flat Appl) u1 t1) (THead
+(Flat Appl) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda
+(_: T).(\lambda (t2: T).(pr0 t1 t2))) u1 t1 (refl_equal T (THead (Flat Appl)
+u1 t1)) (pr0_refl u1) (pr0_refl t1))) x H3)))))))) (\lambda (H0: (pr0 (THead
+(Flat Appl) u1 t1) x)).(\lambda (u0: T).(\lambda (u2: T).(\lambda (t0:
+T).(\lambda (t3: T).(\lambda (k: K).(\lambda (H2: (eq T (THead k u0 t0)
+(THead (Flat Appl) u1 t1))).(\lambda (H3: (eq T (THead k u2 t3) x)).(\lambda
+(H1: (pr0 u0 u2)).(\lambda (H4: (pr0 t0 t3)).(let H5 \def (eq_ind_r T x
+(\lambda (t: T).(pr0 (THead (Flat Appl) u1 t1) t)) H0 (THead k u2 t3) H3) in
+(let H6 \def (eq_ind_r T x (\lambda (t: T).(pr0 (THead (Flat Appl) u1 t1) t))
+H (THead k u2 t3) H3) in (eq_ind T (THead k u2 t3) (\lambda (t: T).(or3
+(ex3_2 T T (\lambda (u3: T).(\lambda (t2: T).(eq T t (THead (Flat Appl) u3
+t2)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_:
+T).(\lambda (t2: T).(pr0 t1 t2)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda
+(z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1
+z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (t2:
+T).(eq T t (THead (Bind Abbr) u3 t2)))))) (\lambda (_: T).(\lambda (_:
+T).(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda
+(z1: T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1 t2)))))) (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 t1
+(THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
+T).(\lambda (u3: T).(\lambda (v2: T).(\lambda (t2: T).(eq T t (THead (Bind b)
+v2 (THead (Flat Appl) (lift (S O) O u3) t2))))))))) (\lambda (_: B).(\lambda
+(_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda (_: T).(pr0
+u1 u3))))))) (\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
+(t2: T).(pr0 z1 t2)))))))))) (let H7 \def (f_equal T K (\lambda (e: T).(match
+e in T return (\lambda (_: T).K) with [(TSort _) \Rightarrow k | (TLRef _)
+\Rightarrow k | (THead k0 _ _) \Rightarrow k0])) (THead k u0 t0) (THead (Flat
+Appl) u1 t1) H2) in ((let H8 \def (f_equal T T (\lambda (e: T).(match e in T
+return (\lambda (_: T).T) with [(TSort _) \Rightarrow u0 | (TLRef _)
+\Rightarrow u0 | (THead _ t _) \Rightarrow t])) (THead k u0 t0) (THead (Flat
+Appl) u1 t1) H2) in ((let H9 \def (f_equal T T (\lambda (e: T).(match e in T
+return (\lambda (_: T).T) with [(TSort _) \Rightarrow t0 | (TLRef _)
+\Rightarrow t0 | (THead _ _ t) \Rightarrow t])) (THead k u0 t0) (THead (Flat
+Appl) u1 t1) H2) in (\lambda (H10: (eq T u0 u1)).(\lambda (H11: (eq K k (Flat
+Appl))).(let H12 \def (eq_ind K k (\lambda (k0: K).(pr0 (THead (Flat Appl) u1
+t1) (THead k0 u2 t3))) H6 (Flat Appl) H11) in (let H13 \def (eq_ind K k
+(\lambda (k0: K).(pr0 (THead (Flat Appl) u1 t1) (THead k0 u2 t3))) H5 (Flat
+Appl) H11) in (eq_ind_r K (Flat Appl) (\lambda (k0: K).(or3 (ex3_2 T T
+(\lambda (u3: T).(\lambda (t2: T).(eq T (THead k0 u2 t3) (THead (Flat Appl)
+u3 t2)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_:
+T).(\lambda (t2: T).(pr0 t1 t2)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda
+(z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1
+z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (t2:
+T).(eq T (THead k0 u2 t3) (THead (Bind Abbr) u3 t2)))))) (\lambda (_:
+T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))))) (\lambda
+(_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1 t2))))))
+(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 t1 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_:
+T).(\lambda (_: T).(\lambda (u3: T).(\lambda (v2: T).(\lambda (t2: T).(eq T
+(THead k0 u2 t3) (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u3)
+t2))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (u3:
+T).(\lambda (_: T).(\lambda (_: T).(pr0 u1 u3))))))) (\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 (t2: T).(pr0 z1 t2)))))))))) (let H14 \def
+(eq_ind T t0 (\lambda (t: T).(pr0 t t3)) H4 t1 H9) in (let H15 \def (eq_ind T
+u0 (\lambda (t: T).(pr0 t u2)) H1 u1 H10) in (or3_intro0 (ex3_2 T T (\lambda
+(u3: T).(\lambda (t2: T).(eq T (THead (Flat Appl) u2 t3) (THead (Flat Appl)
+u3 t2)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_:
+T).(\lambda (t2: T).(pr0 t1 t2)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda
+(z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1
+z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (t2:
+T).(eq T (THead (Flat Appl) u2 t3) (THead (Bind Abbr) u3 t2)))))) (\lambda
+(_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3)))))
+(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1
+t2)))))) (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 t1 (THead (Bind b) y1 z1)))))))) (\lambda (b:
+B).(\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (v2: T).(\lambda
+(t2: T).(eq T (THead (Flat Appl) u2 t3) (THead (Bind b) v2 (THead (Flat Appl)
+(lift (S O) O u3) t2))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_:
+T).(\lambda (u3: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1 u3)))))))
+(\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 (t2: T).(pr0 z1
+t2)))))))) (ex3_2_intro T T (\lambda (u3: T).(\lambda (t2: T).(eq T (THead
+(Flat Appl) u2 t3) (THead (Flat Appl) u3 t2)))) (\lambda (u3: T).(\lambda (_:
+T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2))) u2 t3
+(refl_equal T (THead (Flat Appl) u2 t3)) H15 H14)))) k H11)))))) H8)) H7)) x
+H3))))))))))))) (\lambda (H0: (pr0 (THead (Flat Appl) u1 t1) x)).(\lambda (u:
+T).(\lambda (v1: T).(\lambda (v2: T).(\lambda (t0: T).(\lambda (t3:
+T).(\lambda (H2: (eq T (THead (Flat Appl) v1 (THead (Bind Abst) u t0)) (THead
+(Flat Appl) u1 t1))).(\lambda (H3: (eq T (THead (Bind Abbr) v2 t3)
+x)).(\lambda (H1: (pr0 v1 v2)).(\lambda (H4: (pr0 t0 t3)).(let H5 \def
+(eq_ind_r T x (\lambda (t: T).(pr0 (THead (Flat Appl) u1 t1) t)) H0 (THead
+(Bind Abbr) v2 t3) H3) in (let H6 \def (eq_ind_r T x (\lambda (t: T).(pr0
+(THead (Flat Appl) u1 t1) t)) H (THead (Bind Abbr) v2 t3) H3) in (eq_ind T
+(THead (Bind Abbr) v2 t3) (\lambda (t: T).(or3 (ex3_2 T T (\lambda (u2:
+T).(\lambda (t2: T).(eq T t (THead (Flat Appl) u2 t2)))) (\lambda (u2:
+T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1
+t2)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
+T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1 z1)))))) (\lambda (_:
+T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t2: T).(eq T t (THead (Bind
+Abbr) u2 t2)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
+(_: T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
+T).(\lambda (t2: T).(pr0 z1 t2)))))) (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 t1 (THead (Bind
+b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
+(u2: T).(\lambda (v3: T).(\lambda (t2: T).(eq T t (THead (Bind b) v3 (THead
+(Flat Appl) (lift (S O) O u2) t2))))))))) (\lambda (_: B).(\lambda (_:
+T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1
+u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
+T).(\lambda (v3: T).(\lambda (_: T).(pr0 y1 v3))))))) (\lambda (_:
+B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
+(t2: T).(pr0 z1 t2)))))))))) (let H7 \def (f_equal T T (\lambda (e: T).(match
+e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow v1 | (TLRef _)
+\Rightarrow v1 | (THead _ t _) \Rightarrow t])) (THead (Flat Appl) v1 (THead
+(Bind Abst) u t0)) (THead (Flat Appl) u1 t1) H2) in ((let H8 \def (f_equal T
+T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _)
+\Rightarrow (THead (Bind Abst) u t0) | (TLRef _) \Rightarrow (THead (Bind
+Abst) u t0) | (THead _ _ t) \Rightarrow t])) (THead (Flat Appl) v1 (THead
+(Bind Abst) u t0)) (THead (Flat Appl) u1 t1) H2) in (\lambda (H9: (eq T v1
+u1)).(let H10 \def (eq_ind T v1 (\lambda (t: T).(pr0 t v2)) H1 u1 H9) in (let
+H11 \def (eq_ind_r T t1 (\lambda (t: T).(pr0 (THead (Flat Appl) u1 t) (THead
+(Bind Abbr) v2 t3))) H6 (THead (Bind Abst) u t0) H8) in (let H12 \def
+(eq_ind_r T t1 (\lambda (t: T).(pr0 (THead (Flat Appl) u1 t) (THead (Bind
+Abbr) v2 t3))) H5 (THead (Bind Abst) u t0) H8) in (eq_ind T (THead (Bind
+Abst) u t0) (\lambda (t: T).(or3 (ex3_2 T T (\lambda (u2: T).(\lambda (t2:
+T).(eq T (THead (Bind Abbr) v2 t3) (THead (Flat Appl) u2 t2)))) (\lambda (u2:
+T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t
+t2)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
+T).(\lambda (_: T).(eq T t (THead (Bind Abst) y1 z1)))))) (\lambda (_:
+T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t2: T).(eq T (THead (Bind Abbr)
+v2 t3) (THead (Bind Abbr) u2 t2)))))) (\lambda (_: T).(\lambda (_:
+T).(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda
+(z1: T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1 t2)))))) (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 t
+(THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
+T).(\lambda (u2: T).(\lambda (v3: T).(\lambda (t2: T).(eq T (THead (Bind
+Abbr) v2 t3) (THead (Bind b) v3 (THead (Flat Appl) (lift (S O) O u2)
+t2))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2:
+T).(\lambda (_: T).(\lambda (_: T).(pr0 u1 u2))))))) (\lambda (_: B).(\lambda
+(y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (v3: T).(\lambda (_: T).(pr0
+y1 v3))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_:
+T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1 t2)))))))))) (or3_intro1 (ex3_2 T
+T (\lambda (u2: T).(\lambda (t2: T).(eq T (THead (Bind Abbr) v2 t3) (THead
+(Flat Appl) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda
+(_: T).(\lambda (t2: T).(pr0 (THead (Bind Abst) u t0) t2)))) (ex4_4 T T T T
+(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T
+(THead (Bind Abst) u t0) (THead (Bind Abst) y1 z1)))))) (\lambda (_:
+T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t2: T).(eq T (THead (Bind Abbr)
+v2 t3) (THead (Bind Abbr) u2 t2)))))) (\lambda (_: T).(\lambda (_:
+T).(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda
+(z1: T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1 t2)))))) (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
+(THead (Bind Abst) u t0) (THead (Bind b) y1 z1)))))))) (\lambda (b:
+B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (v3: T).(\lambda
+(t2: T).(eq T (THead (Bind Abbr) v2 t3) (THead (Bind b) v3 (THead (Flat Appl)
+(lift (S O) O u2) t2))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_:
+T).(\lambda (u2: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1 u2)))))))
+(\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
+(v3: T).(\lambda (_: T).(pr0 y1 v3))))))) (\lambda (_: B).(\lambda (_:
+T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1
+t2)))))))) (ex4_4_intro T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda
+(_: T).(\lambda (_: T).(eq T (THead (Bind Abst) u t0) (THead (Bind Abst) y1
+z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t2:
+T).(eq T (THead (Bind Abbr) v2 t3) (THead (Bind Abbr) u2 t2)))))) (\lambda
+(_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2)))))
+(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1
+t2))))) u t0 v2 t3 (refl_equal T (THead (Bind Abst) u t0)) (refl_equal T
+(THead (Bind Abbr) v2 t3)) H10 H4)) t1 H8)))))) H7)) x H3)))))))))))))
+(\lambda (H0: (pr0 (THead (Flat Appl) u1 t1) x)).(\lambda (b: B).(\lambda
+(v1: T).(\lambda (v2: T).(\lambda (u0: T).(\lambda (u2: T).(\lambda (t0:
+T).(\lambda (t3: T).(\lambda (H4: (eq T (THead (Flat Appl) v1 (THead (Bind b)
+u0 t0)) (THead (Flat Appl) u1 t1))).(\lambda (H5: (eq T (THead (Bind b) u2
+(THead (Flat Appl) (lift (S O) O v2) t3)) x)).(\lambda (H1: (not (eq B b
+Abst))).(\lambda (H2: (pr0 v1 v2)).(\lambda (H3: (pr0 u0 u2)).(\lambda (H6:
+(pr0 t0 t3)).(let H7 \def (eq_ind_r T x (\lambda (t: T).(pr0 (THead (Flat
+Appl) u1 t1) t)) H0 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2)
+t3)) H5) in (let H8 \def (eq_ind_r T x (\lambda (t: T).(pr0 (THead (Flat
+Appl) u1 t1) t)) H (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2)
+t3)) H5) in (eq_ind T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2)
+t3)) (\lambda (t: T).(or3 (ex3_2 T T (\lambda (u3: T).(\lambda (t2: T).(eq T
+t (THead (Flat Appl) u3 t2)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3)))
+(\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (ex4_4 T T T T (\lambda (y1:
+T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind
+Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda
+(t2: T).(eq T t (THead (Bind Abbr) u3 t2)))))) (\lambda (_: T).(\lambda (_:
+T).(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda
+(z1: T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1 t2)))))) (ex6_6 B T T T T T
+(\lambda (b0: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
+T).(\lambda (_: T).(not (eq B b0 Abst)))))))) (\lambda (b0: B).(\lambda (y1:
+T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1
+(THead (Bind b0) y1 z1)))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (_:
+T).(\lambda (u3: T).(\lambda (v3: T).(\lambda (t2: T).(eq T t (THead (Bind
+b0) v3 (THead (Flat Appl) (lift (S O) O u3) t2))))))))) (\lambda (_:
+B).(\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda
+(_: T).(pr0 u1 u3))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
+T).(\lambda (_: T).(\lambda (v3: T).(\lambda (_: T).(pr0 y1 v3)))))))
+(\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
+T).(\lambda (t2: T).(pr0 z1 t2)))))))))) (let H9 \def (f_equal T T (\lambda
+(e: T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow v1
+| (TLRef _) \Rightarrow v1 | (THead _ t _) \Rightarrow t])) (THead (Flat
+Appl) v1 (THead (Bind b) u0 t0)) (THead (Flat Appl) u1 t1) H4) in ((let H10
+\def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T)
+with [(TSort _) \Rightarrow (THead (Bind b) u0 t0) | (TLRef _) \Rightarrow
+(THead (Bind b) u0 t0) | (THead _ _ t) \Rightarrow t])) (THead (Flat Appl) v1
+(THead (Bind b) u0 t0)) (THead (Flat Appl) u1 t1) H4) in (\lambda (H11: (eq T
+v1 u1)).(let H12 \def (eq_ind T v1 (\lambda (t: T).(pr0 t v2)) H2 u1 H11) in
+(let H13 \def (eq_ind_r T t1 (\lambda (t: T).(pr0 (THead (Flat Appl) u1 t)
+(THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t3)))) H8 (THead
+(Bind b) u0 t0) H10) in (let H14 \def (eq_ind_r T t1 (\lambda (t: T).(pr0
+(THead (Flat Appl) u1 t) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O
+v2) t3)))) H7 (THead (Bind b) u0 t0) H10) in (eq_ind T (THead (Bind b) u0 t0)
+(\lambda (t: T).(or3 (ex3_2 T T (\lambda (u3: T).(\lambda (t2: T).(eq T
+(THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t3)) (THead (Flat
+Appl) u3 t2)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_:
+T).(\lambda (t2: T).(pr0 t t2)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda
+(z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t (THead (Bind Abst) y1
+z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (t2:
+T).(eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t3)) (THead
+(Bind Abbr) u3 t2)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3:
+T).(\lambda (_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda (z1: T).(\lambda
+(_: T).(\lambda (t2: T).(pr0 z1 t2)))))) (ex6_6 B T T T T T (\lambda (b0:
+B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
+(_: T).(not (eq B b0 Abst)))))))) (\lambda (b0: B).(\lambda (y1: T).(\lambda
+(z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t (THead (Bind
+b0) y1 z1)))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (_: T).(\lambda
+(u3: T).(\lambda (v3: T).(\lambda (t2: T).(eq T (THead (Bind b) u2 (THead
+(Flat Appl) (lift (S O) O v2) t3)) (THead (Bind b0) v3 (THead (Flat Appl)
+(lift (S O) O u3) t2))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_:
+T).(\lambda (u3: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1 u3)))))))
+(\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
+(v3: T).(\lambda (_: T).(pr0 y1 v3))))))) (\lambda (_: B).(\lambda (_:
+T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1
+t2)))))))))) (or3_intro2 (ex3_2 T T (\lambda (u3: T).(\lambda (t2: T).(eq T
+(THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t3)) (THead (Flat
+Appl) u3 t2)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_:
+T).(\lambda (t2: T).(pr0 (THead (Bind b) u0 t0) t2)))) (ex4_4 T T T T
+(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T
+(THead (Bind b) u0 t0) (THead (Bind Abst) y1 z1)))))) (\lambda (_:
+T).(\lambda (_: T).(\lambda (u3: T).(\lambda (t2: T).(eq T (THead (Bind b) u2
+(THead (Flat Appl) (lift (S O) O v2) t3)) (THead (Bind Abbr) u3 t2))))))
+(\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(pr0 u1
+u3))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t2:
+T).(pr0 z1 t2)))))) (ex6_6 B T T T T T (\lambda (b0: B).(\lambda (_:
+T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B
+b0 Abst)))))))) (\lambda (b0: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda
+(_: T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Bind b) u0 t0) (THead
+(Bind b0) y1 z1)))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (_:
+T).(\lambda (u3: T).(\lambda (v3: T).(\lambda (t2: T).(eq T (THead (Bind b)
+u2 (THead (Flat Appl) (lift (S O) O v2) t3)) (THead (Bind b0) v3 (THead (Flat
+Appl) (lift (S O) O u3) t2))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda
+(_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1 u3)))))))
+(\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
+(v3: T).(\lambda (_: T).(pr0 y1 v3))))))) (\lambda (_: B).(\lambda (_:
+T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1
+t2)))))))) (ex6_6_intro B T T T T T (\lambda (b0: B).(\lambda (_: T).(\lambda
+(_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b0
+Abst)))))))) (\lambda (b0: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
+T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Bind b) u0 t0) (THead (Bind
+b0) y1 z1)))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (_: T).(\lambda
+(u3: T).(\lambda (v3: T).(\lambda (t2: T).(eq T (THead (Bind b) u2 (THead
+(Flat Appl) (lift (S O) O v2) t3)) (THead (Bind b0) v3 (THead (Flat Appl)
+(lift (S O) O u3) t2))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_:
+T).(\lambda (u3: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1 u3)))))))
+(\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
+(v3: T).(\lambda (_: T).(pr0 y1 v3))))))) (\lambda (_: B).(\lambda (_:
+T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1
+t2))))))) b u0 t0 v2 u2 t3 H1 (refl_equal T (THead (Bind b) u0 t0))
+(refl_equal T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t3)))
+H12 H3 H6)) t1 H10)))))) H9)) x H5))))))))))))))))) (\lambda (H0: (pr0 (THead
+(Flat Appl) u1 t1) x)).(\lambda (u0: T).(\lambda (u2: T).(\lambda (t0:
+T).(\lambda (t3: T).(\lambda (w: T).(\lambda (H3: (eq T (THead (Bind Abbr) u0
+t0) (THead (Flat Appl) u1 t1))).(\lambda (H4: (eq T (THead (Bind Abbr) u2 w)
+x)).(\lambda (_: (pr0 u0 u2)).(\lambda (_: (pr0 t0 t3)).(\lambda (_: (subst0
+O u2 t3 w)).(let H6 \def (eq_ind_r T x (\lambda (t: T).(pr0 (THead (Flat
+Appl) u1 t1) t)) H0 (THead (Bind Abbr) u2 w) H4) in (let H7 \def (eq_ind_r T
+x (\lambda (t: T).(pr0 (THead (Flat Appl) u1 t1) t)) H (THead (Bind Abbr) u2
+w) H4) in (eq_ind T (THead (Bind Abbr) u2 w) (\lambda (t: T).(or3 (ex3_2 T T
+(\lambda (u3: T).(\lambda (t2: T).(eq T t (THead (Flat Appl) u3 t2))))
+(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t2:
+T).(pr0 t1 t2)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda
+(_: T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1 z1)))))) (\lambda (_:
+T).(\lambda (_: T).(\lambda (u3: T).(\lambda (t2: T).(eq T t (THead (Bind
+Abbr) u3 t2)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda
+(_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
+T).(\lambda (t2: T).(pr0 z1 t2)))))) (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 t1 (THead (Bind
+b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
+(u3: T).(\lambda (v2: T).(\lambda (t2: T).(eq T t (THead (Bind b) v2 (THead
+(Flat Appl) (lift (S O) O u3) t2))))))))) (\lambda (_: B).(\lambda (_:
+T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1
+u3))))))) (\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
+(t2: T).(pr0 z1 t2)))))))))) (let H8 \def (eq_ind T (THead (Bind Abbr) u0 t0)
+(\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _)
+\Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow
+(match k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow True |
+(Flat _) \Rightarrow False])])) I (THead (Flat Appl) u1 t1) H3) in (False_ind
+(or3 (ex3_2 T T (\lambda (u3: T).(\lambda (t2: T).(eq T (THead (Bind Abbr) u2
+w) (THead (Flat Appl) u3 t2)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1
+u3))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (ex4_4 T T T T (\lambda
+(y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead
+(Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3:
+T).(\lambda (t2: T).(eq T (THead (Bind Abbr) u2 w) (THead (Bind Abbr) u3
+t2)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_:
+T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda
+(t2: T).(pr0 z1 t2)))))) (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 t1 (THead (Bind b) y1 z1))))))))
+(\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda
+(v2: T).(\lambda (t2: T).(eq T (THead (Bind Abbr) u2 w) (THead (Bind b) v2
+(THead (Flat Appl) (lift (S O) O u3) t2))))))))) (\lambda (_: B).(\lambda (_:
+T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1
+u3))))))) (\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
+(t2: T).(pr0 z1 t2))))))))) H8)) x H4)))))))))))))) (\lambda (_: (pr0 (THead
+(Flat Appl) u1 t1) x)).(\lambda (b: B).(\lambda (t0: T).(\lambda (t3:
+T).(\lambda (u: T).(\lambda (H2: (eq T (THead (Bind b) u (lift (S O) O t0))
+(THead (Flat Appl) u1 t1))).(\lambda (H3: (eq T t3 x)).(\lambda (_: (not (eq
+B b Abst))).(\lambda (H4: (pr0 t0 t3)).(let H5 \def (eq_ind T t3 (\lambda (t:
+T).(pr0 t0 t)) H4 x H3) in (let H6 \def (eq_ind T (THead (Bind b) u (lift (S
+O) O t0)) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with
+[(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _)
+\Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind _)
+\Rightarrow True | (Flat _) \Rightarrow False])])) I (THead (Flat Appl) u1
+t1) H2) in (False_ind (or3 (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T
+x (THead (Flat Appl) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2)))
+(\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (ex4_4 T T T T (\lambda (y1:
+T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind
+Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
+(t2: T).(eq T x (THead (Bind Abbr) u2 t2)))))) (\lambda (_: T).(\lambda (_:
+T).(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda
+(z1: T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1 t2)))))) (ex6_6 B T T T T T
+(\lambda (b0: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
+T).(\lambda (_: T).(not (eq B b0 Abst)))))))) (\lambda (b0: B).(\lambda (y1:
+T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1
+(THead (Bind b0) y1 z1)))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (_:
+T).(\lambda (u2: T).(\lambda (v2: T).(\lambda (t2: T).(eq T x (THead (Bind
+b0) v2 (THead (Flat Appl) (lift (S O) O u2) t2))))))))) (\lambda (_:
+B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(\lambda
+(_: T).(pr0 u1 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 (t2: T).(pr0 z1 t2))))))))) H6)))))))))))) (\lambda (_: (pr0
+(THead (Flat Appl) u1 t1) x)).(\lambda (t0: T).(\lambda (t3: T).(\lambda (u:
+T).(\lambda (H1: (eq T (THead (Flat Cast) u t0) (THead (Flat Appl) u1
+t1))).(\lambda (H2: (eq T t3 x)).(\lambda (H3: (pr0 t0 t3)).(let H4 \def
+(eq_ind T t3 (\lambda (t: T).(pr0 t0 t)) H3 x H2) in (let H5 \def (eq_ind T
+(THead (Flat Cast) u t0) (\lambda (ee: T).(match ee in T return (\lambda (_:
+T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False |
+(THead k _ _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with
+[(Bind _) \Rightarrow False | (Flat f) \Rightarrow (match f in F return
+(\lambda (_: F).Prop) with [Appl \Rightarrow False | Cast \Rightarrow
+True])])])) I (THead (Flat Appl) u1 t1) H1) in (False_ind (or3 (ex3_2 T T
+(\lambda (u2: T).(\lambda (t2: T).(eq T x (THead (Flat Appl) u2 t2))))
+(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2:
+T).(pr0 t1 t2)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda
+(_: T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1 z1)))))) (\lambda (_:
+T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t2: T).(eq T x (THead (Bind
+Abbr) u2 t2)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
+(_: T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
+T).(\lambda (t2: T).(pr0 z1 t2)))))) (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 t1 (THead (Bind
+b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
+(u2: T).(\lambda (v2: T).(\lambda (t2: T).(eq T x (THead (Bind b) v2 (THead
+(Flat Appl) (lift (S O) O u2) t2))))))))) (\lambda (_: B).(\lambda (_:
+T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1
+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
+(t2: T).(pr0 z1 t2))))))))) H5)))))))))) H)))).