-T).(\lambda (u2: T).(subst0 O v u1 u2)))))) (\lambda (_: F).(\lambda (e1:
-C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 O v e1 e2))))))
-x3 x4 x5 x6 x7 (refl_equal C (CHead x5 (Flat x3) x7)) (drop_drop (Bind b) n0
-c (CHead x4 (Flat x3) x6) H16 t) H17 H18)) e H15)))))))))) H14)) H13))))))))
-(\lambda (f: F).(\lambda (H8: (eq nat (S n0) (s (Flat f) x2))).(\lambda (H9:
-(drop (r (Flat f) n0) O x1 e)).(let H10 \def (f_equal nat nat (\lambda (e0:
-nat).e0) (S n0) x2 H8) in (let H11 \def (eq_ind_r nat x2 (\lambda (n1:
-nat).(csubst0 n1 v c x1)) H6 (S n0) H10) in (let H12 \def (eq_ind_r nat x2
-(\lambda (n1: nat).(subst0 n1 v t x0)) H5 (S n0) H10) in (let H13 \def (H x1
-v H11 e H9) in (or4_ind (drop (S n0) O c e) (ex3_4 F C T T (\lambda (f0:
-F).(\lambda (e0: C).(\lambda (_: T).(\lambda (u2: T).(eq C e (CHead e0 (Flat
-f0) u2)))))) (\lambda (f0: F).(\lambda (e0: C).(\lambda (u1: T).(\lambda (_:
-T).(drop (S n0) O c (CHead e0 (Flat f0) u1)))))) (\lambda (_: F).(\lambda (_:
-C).(\lambda (u1: T).(\lambda (u2: T).(subst0 O v u1 u2)))))) (ex3_4 F C C T
-(\lambda (f0: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(eq C e
-(CHead e2 (Flat f0) u)))))) (\lambda (f0: F).(\lambda (e1: C).(\lambda (_:
-C).(\lambda (u: T).(drop (S n0) O c (CHead e1 (Flat f0) u)))))) (\lambda (_:
-F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 O v e1 e2))))))
-(ex4_5 F C C T T (\lambda (f0: F).(\lambda (_: C).(\lambda (e2: C).(\lambda
-(_: T).(\lambda (u2: T).(eq C e (CHead e2 (Flat f0) u2))))))) (\lambda (f0:
-F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (_: T).(drop (S
-n0) O c (CHead e1 (Flat f0) u1))))))) (\lambda (_: F).(\lambda (_:
-C).(\lambda (_: C).(\lambda (u1: T).(\lambda (u2: T).(subst0 O v u1 u2))))))
-(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
-(_: T).(csubst0 O v e1 e2))))))) (or4 (drop (S n0) O (CHead c (Flat f) t) e)
-(ex3_4 F C T T (\lambda (f0: F).(\lambda (e0: C).(\lambda (_: T).(\lambda
-(u2: T).(eq C e (CHead e0 (Flat f0) u2)))))) (\lambda (f0: F).(\lambda (e0:
-C).(\lambda (u1: T).(\lambda (_: T).(drop (S n0) O (CHead c (Flat f) t)
-(CHead e0 (Flat f0) u1)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u1:
-T).(\lambda (u2: T).(subst0 O v u1 u2)))))) (ex3_4 F C C T (\lambda (f0:
-F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(eq C e (CHead e2 (Flat
-f0) u)))))) (\lambda (f0: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u:
-T).(drop (S n0) O (CHead c (Flat f) t) (CHead e1 (Flat f0) u)))))) (\lambda
-(_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 O v e1
-e2)))))) (ex4_5 F C C T T (\lambda (f0: F).(\lambda (_: C).(\lambda (e2:
-C).(\lambda (_: T).(\lambda (u2: T).(eq C e (CHead e2 (Flat f0) u2)))))))
-(\lambda (f0: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(\lambda
-(_: T).(drop (S n0) O (CHead c (Flat f) t) (CHead e1 (Flat f0) u1)))))))
-(\lambda (_: F).(\lambda (_: C).(\lambda (_: C).(\lambda (u1: T).(\lambda
-(u2: T).(subst0 O v u1 u2)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda
-(e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 O v e1 e2)))))))) (\lambda
-(H14: (drop (S n0) O c e)).(or4_intro0 (drop (S n0) O (CHead c (Flat f) t) e)
-(ex3_4 F C T T (\lambda (f0: F).(\lambda (e0: C).(\lambda (_: T).(\lambda
-(u2: T).(eq C e (CHead e0 (Flat f0) u2)))))) (\lambda (f0: F).(\lambda (e0:
-C).(\lambda (u1: T).(\lambda (_: T).(drop (S n0) O (CHead c (Flat f) t)
-(CHead e0 (Flat f0) u1)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u1:
-T).(\lambda (u2: T).(subst0 O v u1 u2)))))) (ex3_4 F C C T (\lambda (f0:
-F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(eq C e (CHead e2 (Flat
-f0) u)))))) (\lambda (f0: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u:
-T).(drop (S n0) O (CHead c (Flat f) t) (CHead e1 (Flat f0) u)))))) (\lambda
-(_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 O v e1
-e2)))))) (ex4_5 F C C T T (\lambda (f0: F).(\lambda (_: C).(\lambda (e2:
-C).(\lambda (_: T).(\lambda (u2: T).(eq C e (CHead e2 (Flat f0) u2)))))))
-(\lambda (f0: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(\lambda
-(_: T).(drop (S n0) O (CHead c (Flat f) t) (CHead e1 (Flat f0) u1)))))))
-(\lambda (_: F).(\lambda (_: C).(\lambda (_: C).(\lambda (u1: T).(\lambda
-(u2: T).(subst0 O v u1 u2)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda
-(e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 O v e1 e2))))))) (drop_drop
-(Flat f) n0 c e H14 t))) (\lambda (H14: (ex3_4 F C T T (\lambda (f0:
-F).(\lambda (e0: C).(\lambda (_: T).(\lambda (u2: T).(eq C e (CHead e0 (Flat
-f0) u2)))))) (\lambda (f0: F).(\lambda (e0: C).(\lambda (u1: T).(\lambda (_:
-T).(drop (S n0) O c (CHead e0 (Flat f0) u1)))))) (\lambda (_: F).(\lambda (_:
-C).(\lambda (u1: T).(\lambda (u2: T).(subst0 O v u1 u2))))))).(ex3_4_ind F C
-T T (\lambda (f0: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (u2: T).(eq C
-e (CHead e0 (Flat f0) u2)))))) (\lambda (f0: F).(\lambda (e0: C).(\lambda
-(u1: T).(\lambda (_: T).(drop (S n0) O c (CHead e0 (Flat f0) u1))))))
-(\lambda (_: F).(\lambda (_: C).(\lambda (u1: T).(\lambda (u2: T).(subst0 O v
-u1 u2))))) (or4 (drop (S n0) O (CHead c (Flat f) t) e) (ex3_4 F C T T
-(\lambda (f0: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (u2: T).(eq C e
-(CHead e0 (Flat f0) u2)))))) (\lambda (f0: F).(\lambda (e0: C).(\lambda (u1:
-T).(\lambda (_: T).(drop (S n0) O (CHead c (Flat f) t) (CHead e0 (Flat f0)
-u1)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u1: T).(\lambda (u2:
-T).(subst0 O v u1 u2)))))) (ex3_4 F C C T (\lambda (f0: F).(\lambda (_:
-C).(\lambda (e2: C).(\lambda (u: T).(eq C e (CHead e2 (Flat f0) u))))))
-(\lambda (f0: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(drop (S
-n0) O (CHead c (Flat f) t) (CHead e1 (Flat f0) u)))))) (\lambda (_:
-F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 O v e1 e2))))))
-(ex4_5 F C C T T (\lambda (f0: F).(\lambda (_: C).(\lambda (e2: C).(\lambda
-(_: T).(\lambda (u2: T).(eq C e (CHead e2 (Flat f0) u2))))))) (\lambda (f0:
-F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (_: T).(drop (S
-n0) O (CHead c (Flat f) t) (CHead e1 (Flat f0) u1))))))) (\lambda (_:
-F).(\lambda (_: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (u2: T).(subst0
-O v u1 u2)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda
-(_: T).(\lambda (_: T).(csubst0 O v e1 e2)))))))) (\lambda (x3: F).(\lambda
-(x4: C).(\lambda (x5: T).(\lambda (x6: T).(\lambda (H15: (eq C e (CHead x4
-(Flat x3) x6))).(\lambda (H16: (drop (S n0) O c (CHead x4 (Flat x3)
-x5))).(\lambda (H17: (subst0 O v x5 x6)).(eq_ind_r C (CHead x4 (Flat x3) x6)
-(\lambda (c0: C).(or4 (drop (S n0) O (CHead c (Flat f) t) c0) (ex3_4 F C T T
-(\lambda (f0: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (u2: T).(eq C c0
-(CHead e0 (Flat f0) u2)))))) (\lambda (f0: F).(\lambda (e0: C).(\lambda (u1:
-T).(\lambda (_: T).(drop (S n0) O (CHead c (Flat f) t) (CHead e0 (Flat f0)
-u1)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u1: T).(\lambda (u2:
-T).(subst0 O v u1 u2)))))) (ex3_4 F C C T (\lambda (f0: F).(\lambda (_:
-C).(\lambda (e2: C).(\lambda (u: T).(eq C c0 (CHead e2 (Flat f0) u))))))
-(\lambda (f0: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(drop (S
-n0) O (CHead c (Flat f) t) (CHead e1 (Flat f0) u)))))) (\lambda (_:
-F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 O v e1 e2))))))
-(ex4_5 F C C T T (\lambda (f0: F).(\lambda (_: C).(\lambda (e2: C).(\lambda
-(_: T).(\lambda (u2: T).(eq C c0 (CHead e2 (Flat f0) u2))))))) (\lambda (f0:
-F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (_: T).(drop (S
-n0) O (CHead c (Flat f) t) (CHead e1 (Flat f0) u1))))))) (\lambda (_:
-F).(\lambda (_: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (u2: T).(subst0
-O v u1 u2)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda
-(_: T).(\lambda (_: T).(csubst0 O v e1 e2))))))))) (or4_intro1 (drop (S n0) O
-(CHead c (Flat f) t) (CHead x4 (Flat x3) x6)) (ex3_4 F C T T (\lambda (f0:
-F).(\lambda (e0: C).(\lambda (_: T).(\lambda (u2: T).(eq C (CHead x4 (Flat
-x3) x6) (CHead e0 (Flat f0) u2)))))) (\lambda (f0: F).(\lambda (e0:
-C).(\lambda (u1: T).(\lambda (_: T).(drop (S n0) O (CHead c (Flat f) t)
-(CHead e0 (Flat f0) u1)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u1:
-T).(\lambda (u2: T).(subst0 O v u1 u2)))))) (ex3_4 F C C T (\lambda (f0:
-F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(eq C (CHead x4 (Flat x3)
-x6) (CHead e2 (Flat f0) u)))))) (\lambda (f0: F).(\lambda (e1: C).(\lambda
-(_: C).(\lambda (u: T).(drop (S n0) O (CHead c (Flat f) t) (CHead e1 (Flat
-f0) u)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: