-(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
+(THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
+T).(\lambda (u2: T).(\lambda (v3: T).(\lambda (t3: T).(eq T v2 (THead (Bind
+b) v3 (THead (Flat Appl) (lift (S O) O u2) t3))))))))) (\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 (t3: T).(pr0 z1 t3))))))))))) H9 (THead (Bind Abst) u t0) H7) in
+(eq_ind T (THead (Bind Abst) u t0) (\lambda (t: T).(or3 (ex3_2 T T (\lambda
+(u2: T).(\lambda (t3: T).(eq T (THead (Bind Abbr) v2 t2) (THead (Flat Appl)
+u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_:
+T).(\lambda (t3: T).(pr0 t t3)))) (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 (t3:
+T).(eq T (THead (Bind Abbr) v2 t2) (THead (Bind Abbr) u2 t3)))))) (\lambda
+(_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2)))))
+(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1
+t3)))))) (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
+(t3: T).(eq T (THead (Bind Abbr) v2 t2) (THead (Bind b) v3 (THead (Flat Appl)
+(lift (S O) O u2) t3))))))))) (\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 (t3: T).(pr0 z1
+t3)))))))))) (or3_intro1 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T
+(THead (Bind Abbr) v2 t2) (THead (Flat Appl) u2 t3)))) (\lambda (u2:
+T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(pr0 (THead
+(Bind Abst) u t0) t3)))) (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 (t3: T).(eq T (THead (Bind Abbr) v2 t2) (THead (Bind Abbr) u2
+t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_:
+T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda
+(t3: T).(pr0 z1 t3)))))) (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 (t3: T).(eq T (THead (Bind
+Abbr) v2 t2) (THead (Bind b) v3 (THead (Flat Appl) (lift (S O) O u2)
+t3))))))))) (\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 (t3: T).(pr0 z1 t3)))))))) (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 (t3: T).(eq T (THead (Bind Abbr)
+v2 t2) (THead (Bind Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_:
+T).(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda
+(z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3))))) u t0 v2 t2
+(refl_equal T (THead (Bind Abst) u t0)) (refl_equal T (THead (Bind Abbr) v2
+t2)) H10 H3)) t1 H7))))))) H6)))))))))))) (\lambda (b: B).(\lambda (H1: (not
+(eq B b Abst))).(\lambda (v1: T).(\lambda (v2: T).(\lambda (H2: (pr0 v1
+v2)).(\lambda (H3: (((eq T v1 (THead (Flat Appl) u1 t1)) \to (or3 (ex3_2 T T
+(\lambda (u2: T).(\lambda (t2: T).(eq T v2 (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 v2 (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 (v3: T).(\lambda (t2: T).(eq T v2 (THead (Bind b0) 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)))))))))))).(\lambda (u0: T).(\lambda (u2: T).(\lambda
+(H4: (pr0 u0 u2)).(\lambda (H5: (((eq T u0 (THead (Flat Appl) u1 t1)) \to
+(or3 (ex3_2 T T (\lambda (u3: T).(\lambda (t2: T).(eq T u2 (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 u2 (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 u2 (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)))))))))))).(\lambda (t0: T).(\lambda (t2:
+T).(\lambda (H6: (pr0 t0 t2)).(\lambda (H7: (((eq T t0 (THead (Flat Appl) u1
+t1)) \to (or3 (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead
+(Flat Appl) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda
+(_: T).(\lambda (t3: T).(pr0 t1 t3)))) (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
+(t3: T).(eq T t2 (THead (Bind Abbr) u3 t3)))))) (\lambda (_: T).(\lambda (_:
+T).(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda
+(z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3)))))) (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 (t3: T).(eq T t2 (THead (Bind
+b0) v3 (THead (Flat Appl) (lift (S O) O u3) t3))))))))) (\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 (t3: T).(pr0 z1 t3)))))))))))).(\lambda (H8: (eq T (THead (Flat
+Appl) v1 (THead (Bind b) u0 t0)) (THead (Flat Appl) u1 t1))).(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) H8) 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)
+H8) in (\lambda (H11: (eq T v1 u1)).(let H12 \def (eq_ind T v1 (\lambda (t:
+T).((eq T t (THead (Flat Appl) u1 t1)) \to (or3 (ex3_2 T T (\lambda (u3:
+T).(\lambda (t3: T).(eq T v2 (THead (Flat Appl) u3 t3)))) (\lambda (u3:
+T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1
+t3)))) (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 (t3: T).(eq T v2 (THead (Bind
+Abbr) u3 t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda
+(_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
+T).(\lambda (t3: T).(pr0 z1 t3)))))) (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 (t3: T).(eq T v2 (THead (Bind b0) v3 (THead
+(Flat Appl) (lift (S O) O u3) t3))))))))) (\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
+(t3: T).(pr0 z1 t3))))))))))) H3 u1 H11) in (let H13 \def (eq_ind T v1
+(\lambda (t: T).(pr0 t v2)) H2 u1 H11) in (let H14 \def (eq_ind_r T t1
+(\lambda (t: T).((eq T t0 (THead (Flat Appl) u1 t)) \to (or3 (ex3_2 T T
+(\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u3 t3))))
+(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3:
+T).(pr0 t t3)))) (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 (t3: T).(eq T t2 (THead (Bind
+Abbr) u3 t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda
+(_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
+T).(\lambda (t3: T).(pr0 z1 t3)))))) (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 (t3: T).(eq T t2 (THead (Bind b0) v3 (THead
+(Flat Appl) (lift (S O) O u3) t3))))))))) (\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
+(t3: T).(pr0 z1 t3))))))))))) H7 (THead (Bind b) u0 t0) H10) in (let H15 \def
+(eq_ind_r T t1 (\lambda (t: T).((eq T u0 (THead (Flat Appl) u1 t)) \to (or3
+(ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T u2 (THead (Flat Appl) u3
+t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_:
+T).(\lambda (t3: T).(pr0 t t3)))) (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 (t3:
+T).(eq T u2 (THead (Bind Abbr) u3 t3)))))) (\lambda (_: T).(\lambda (_:
+T).(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda
+(z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3)))))) (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 (t3: T).(eq T u2 (THead (Bind
+b0) v3 (THead (Flat Appl) (lift (S O) O u3) t3))))))))) (\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 (t3: T).(pr0 z1 t3))))))))))) H5 (THead (Bind b) u0 t0) H10) in
+(let H16 \def (eq_ind_r T t1 (\lambda (t: T).((eq T u1 (THead (Flat Appl) u1
+t)) \to (or3 (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T v2 (THead
+(Flat Appl) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda
+(_: T).(\lambda (t3: T).(pr0 t t3)))) (ex4_4 T T T T (\lambda (y1:
+T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t (THead (Bind