-(H: (pr2 c (THead (Flat Appl) u1 t1) x)).(let H0 \def (match H in pr2 return
-(\lambda (c0: C).(\lambda (t: T).(\lambda (t0: T).(\lambda (_: (pr2 c0 t
-t0)).((eq C c0 c) \to ((eq T t (THead (Flat Appl) u1 t1)) \to ((eq T t0 x)
-\to (or3 (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T x (THead (Flat
-Appl) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c u1 u2))) (\lambda (_:
-T).(\lambda (t2: T).(pr2 c 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).(pr2 c u1 u2))))) (\lambda (_:
-T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t2: T).(\forall (b: B).(\forall
-(u: T).(pr2 (CHead c (Bind b) u) 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 (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T x (THead (Bind b)
-y2 (THead (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_: B).(\lambda
-(_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2
-c u1 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
-T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1 y2))))))) (\lambda (b:
-B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda (_: T).(\lambda
-(y2: T).(pr2 (CHead c (Bind b) y2) z1 z2)))))))))))))))) with [(pr2_free c0
-t0 t2 H0) \Rightarrow (\lambda (H1: (eq C c0 c)).(\lambda (H2: (eq T t0
-(THead (Flat Appl) u1 t1))).(\lambda (H3: (eq T t2 x)).(eq_ind C c (\lambda
-(_: C).((eq T t0 (THead (Flat Appl) u1 t1)) \to ((eq T t2 x) \to ((pr0 t0 t2)
-\to (or3 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T x (THead (Flat
-Appl) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c u1 u2))) (\lambda (_:
-T).(\lambda (t3: T).(pr2 c 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 (u2: T).(\lambda (t3:
-T).(eq T x (THead (Bind Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_:
-T).(\lambda (u2: T).(\lambda (_: T).(pr2 c u1 u2))))) (\lambda (_:
-T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: T).(\forall (b: B).(\forall
-(u: T).(pr2 (CHead c (Bind b) u) 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 t1
-(THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
-T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T x (THead (Bind b)
-y2 (THead (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_: B).(\lambda
-(_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2
-c u1 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
-T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1 y2))))))) (\lambda (b:
-B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda (_: T).(\lambda
-(y2: T).(pr2 (CHead c (Bind b) y2) z1 z2))))))))))))) (\lambda (H4: (eq T t0
-(THead (Flat Appl) u1 t1))).(eq_ind T (THead (Flat Appl) u1 t1) (\lambda (t:
-T).((eq T t2 x) \to ((pr0 t t2) \to (or3 (ex3_2 T T (\lambda (u2: T).(\lambda
-(t3: T).(eq T x (THead (Flat Appl) u2 t3)))) (\lambda (u2: T).(\lambda (_:
-T).(pr2 c u1 u2))) (\lambda (_: T).(\lambda (t3: T).(pr2 c 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
-(u2: T).(\lambda (t3: T).(eq T x (THead (Bind Abbr) u2 t3)))))) (\lambda (_:
-T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c u1 u2)))))
-(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: T).(\forall
-(b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) 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 t1 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda
-(_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T x (THead
-(Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_:
-B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
-(_: T).(pr2 c u1 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
-T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1 y2)))))))
-(\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
-(_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1 z2)))))))))))) (\lambda
-(H5: (eq T t2 x)).(eq_ind T x (\lambda (t: T).((pr0 (THead (Flat Appl) u1 t1)
-t) \to (or3 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T x (THead (Flat
-Appl) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c u1 u2))) (\lambda (_:
-T).(\lambda (t3: T).(pr2 c 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 (u2: T).(\lambda (t3:
-T).(eq T x (THead (Bind Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_:
-T).(\lambda (u2: T).(\lambda (_: T).(pr2 c u1 u2))))) (\lambda (_:
-T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: T).(\forall (b: B).(\forall
-(u: T).(pr2 (CHead c (Bind b) u) 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 t1
-(THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
-T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T x (THead (Bind b)
-y2 (THead (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_: B).(\lambda
-(_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2
-c u1 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
-T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1 y2))))))) (\lambda (b:
-B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda (_: T).(\lambda
-(y2: T).(pr2 (CHead c (Bind b) y2) z1 z2))))))))))) (\lambda (H6: (pr0 (THead
-(Flat Appl) u1 t1) x)).(or3_ind (ex3_2 T T (\lambda (u2: T).(\lambda (t3:
-T).(eq T x (THead (Flat Appl) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0
-u1 u2))) (\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 (u2:
-T).(\lambda (t3: T).(eq T x (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 t1 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_:
-T).(\lambda (_: T).(\lambda (u2: T).(\lambda (v2: T).(\lambda (t3: T).(eq T x
-(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 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 (t3: T).(pr0 z1 t3)))))))) (or3 (ex3_2 T T
-(\lambda (u2: T).(\lambda (t3: T).(eq T x (THead (Flat Appl) u2 t3))))
-(\lambda (u2: T).(\lambda (_: T).(pr2 c u1 u2))) (\lambda (_: T).(\lambda
-(t3: T).(pr2 c 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 (u2: T).(\lambda (t3: T).(eq T x
-(THead (Bind Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
-T).(\lambda (_: T).(pr2 c u1 u2))))) (\lambda (_: T).(\lambda (z1:
-T).(\lambda (_: T).(\lambda (t3: T).(\forall (b: B).(\forall (u: T).(pr2
-(CHead c (Bind b) u) 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 t1 (THead (Bind
-b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
-(z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T x (THead (Bind b) y2 (THead
-(Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_: B).(\lambda (_:
-T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c u1
-u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
-T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1 y2))))))) (\lambda (b:
-B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda (_: T).(\lambda
-(y2: T).(pr2 (CHead c (Bind b) y2) z1 z2))))))))) (\lambda (H7: (ex3_2 T T
-(\lambda (u2: T).(\lambda (t3: T).(eq T x (THead (Flat Appl) u2 t3))))
-(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3:
-T).(pr0 t1 t3))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t3: T).(eq T x
-(THead (Flat Appl) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2)))
-(\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3))) (or3 (ex3_2 T T (\lambda (u2:
-T).(\lambda (t3: T).(eq T x (THead (Flat Appl) u2 t3)))) (\lambda (u2:
-T).(\lambda (_: T).(pr2 c u1 u2))) (\lambda (_: T).(\lambda (t3: T).(pr2 c t1
-t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: