-(Bind b) i0) (s k (S n0))) v e1 e2))))))))))))))).(\lambda (H: (lt (S n0) (s
-(Bind b) i0))).(let H19 \def (IHn i0 (le_S_n (S n0) i0 H) c c0 v H16 e H2) in
-(or4_ind (drop n0 O c0 e) (ex3_4 K C T T (\lambda (k: K).(\lambda (e0:
-C).(\lambda (u0: T).(\lambda (_: T).(eq C e (CHead e0 k u0)))))) (\lambda (k:
-K).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(drop n0 O c0 (CHead e0 k
-w)))))) (\lambda (k: K).(\lambda (_: C).(\lambda (u0: T).(\lambda (w:
-T).(subst0 (minus i0 (s k n0)) v u0 w)))))) (ex3_4 K C C T (\lambda (k:
-K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u0: T).(eq C e (CHead e1 k
-u0)))))) (\lambda (k: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (u0:
-T).(drop n0 O c0 (CHead e2 k u0)))))) (\lambda (k: K).(\lambda (e1:
-C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (minus i0 (s k n0)) v e1
-e2)))))) (ex4_5 K C C T T (\lambda (k: K).(\lambda (e1: C).(\lambda (_:
-C).(\lambda (u0: T).(\lambda (_: T).(eq C e (CHead e1 k u0))))))) (\lambda
-(k: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(drop
-n0 O c0 (CHead e2 k w))))))) (\lambda (k: K).(\lambda (_: C).(\lambda (_:
-C).(\lambda (u0: T).(\lambda (w: T).(subst0 (minus i0 (s k n0)) v u0 w))))))
-(\lambda (k: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
-(_: T).(csubst0 (minus i0 (s k n0)) v e1 e2))))))) (or4 (drop (S n0) O (CHead
-c0 (Bind b) t) e) (ex3_4 K C T T (\lambda (k: K).(\lambda (e0: C).(\lambda
-(u0: T).(\lambda (_: T).(eq C e (CHead e0 k u0)))))) (\lambda (k: K).(\lambda
-(e0: C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead c0 (Bind b) t)
-(CHead e0 k w)))))) (\lambda (k: K).(\lambda (_: C).(\lambda (u0: T).(\lambda
-(w: T).(subst0 (minus (s (Bind b) i0) (s k (S n0))) v u0 w)))))) (ex3_4 K C C
-T (\lambda (k: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u0: T).(eq C e
-(CHead e1 k u0)))))) (\lambda (k: K).(\lambda (_: C).(\lambda (e2:
-C).(\lambda (u0: T).(drop (S n0) O (CHead c0 (Bind b) t) (CHead e2 k u0))))))
-(\lambda (k: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0
-(minus (s (Bind b) i0) (s k (S n0))) v e1 e2)))))) (ex4_5 K C C T T (\lambda
-(k: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(eq
-C e (CHead e1 k u0))))))) (\lambda (k: K).(\lambda (_: C).(\lambda (e2:
-C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead c0 (Bind b) t)
-(CHead e2 k w))))))) (\lambda (k: K).(\lambda (_: C).(\lambda (_: C).(\lambda
-(u0: T).(\lambda (w: T).(subst0 (minus (s (Bind b) i0) (s k (S n0))) v u0
-w)))))) (\lambda (k: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
-T).(\lambda (_: T).(csubst0 (minus (s (Bind b) i0) (s k (S n0))) v e1
-e2)))))))) (\lambda (H20: (drop n0 O c0 e)).(or4_intro0 (drop (S n0) O (CHead
-c0 (Bind b) t) e) (ex3_4 K C T T (\lambda (k: K).(\lambda (e0: C).(\lambda
-(u0: T).(\lambda (_: T).(eq C e (CHead e0 k u0)))))) (\lambda (k: K).(\lambda
-(e0: C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead c0 (Bind b) t)
-(CHead e0 k w)))))) (\lambda (k: K).(\lambda (_: C).(\lambda (u0: T).(\lambda
-(w: T).(subst0 (minus (s (Bind b) i0) (s k (S n0))) v u0 w)))))) (ex3_4 K C C
-T (\lambda (k: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u0: T).(eq C e
-(CHead e1 k u0)))))) (\lambda (k: K).(\lambda (_: C).(\lambda (e2:
-C).(\lambda (u0: T).(drop (S n0) O (CHead c0 (Bind b) t) (CHead e2 k u0))))))
-(\lambda (k: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0
-(minus (s (Bind b) i0) (s k (S n0))) v e1 e2)))))) (ex4_5 K C C T T (\lambda
-(k: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(eq
-C e (CHead e1 k u0))))))) (\lambda (k: K).(\lambda (_: C).(\lambda (e2:
-C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead c0 (Bind b) t)
-(CHead e2 k w))))))) (\lambda (k: K).(\lambda (_: C).(\lambda (_: C).(\lambda
-(u0: T).(\lambda (w: T).(subst0 (minus (s (Bind b) i0) (s k (S n0))) v u0
-w)))))) (\lambda (k: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
-T).(\lambda (_: T).(csubst0 (minus (s (Bind b) i0) (s k (S n0))) v e1
-e2))))))) (drop_drop (Bind b) n0 c0 e H20 t))) (\lambda (H20: (ex3_4 K C T T
-(\lambda (k: K).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C e
-(CHead e0 k u)))))) (\lambda (k: K).(\lambda (e0: C).(\lambda (_: T).(\lambda
-(w: T).(drop n0 O c0 (CHead e0 k w)))))) (\lambda (k: K).(\lambda (_:
-C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus i0 (s k n0)) v u
-w))))))).(ex3_4_ind K C T T (\lambda (k: K).(\lambda (e0: C).(\lambda (u0:
-T).(\lambda (_: T).(eq C e (CHead e0 k u0)))))) (\lambda (k: K).(\lambda (e0:
-C).(\lambda (_: T).(\lambda (w: T).(drop n0 O c0 (CHead e0 k w)))))) (\lambda
-(k: K).(\lambda (_: C).(\lambda (u0: T).(\lambda (w: T).(subst0 (minus i0 (s
-k n0)) v u0 w))))) (or4 (drop (S n0) O (CHead c0 (Bind b) t) e) (ex3_4 K C T
-T (\lambda (k: K).(\lambda (e0: C).(\lambda (u0: T).(\lambda (_: T).(eq C e
-(CHead e0 k u0)))))) (\lambda (k: K).(\lambda (e0: C).(\lambda (_:
-T).(\lambda (w: T).(drop (S n0) O (CHead c0 (Bind b) t) (CHead e0 k w))))))
-(\lambda (k: K).(\lambda (_: C).(\lambda (u0: T).(\lambda (w: T).(subst0
-(minus (s (Bind b) i0) (s k (S n0))) v u0 w)))))) (ex3_4 K C C T (\lambda (k:
-K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u0: T).(eq C e (CHead e1 k
-u0)))))) (\lambda (k: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (u0:
-T).(drop (S n0) O (CHead c0 (Bind b) t) (CHead e2 k u0)))))) (\lambda (k:
-K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (minus (s (Bind
-b) i0) (s k (S n0))) v e1 e2)))))) (ex4_5 K C C T T (\lambda (k: K).(\lambda
-(e1: C).(\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(eq C e (CHead e1 k
-u0))))))) (\lambda (k: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (_:
-T).(\lambda (w: T).(drop (S n0) O (CHead c0 (Bind b) t) (CHead e2 k w)))))))
-(\lambda (k: K).(\lambda (_: C).(\lambda (_: C).(\lambda (u0: T).(\lambda (w:
-T).(subst0 (minus (s (Bind b) i0) (s k (S n0))) v u0 w)))))) (\lambda (k:
-K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0
-(minus (s (Bind b) i0) (s k (S n0))) v e1 e2)))))))) (\lambda (x0:
-K).(\lambda (x1: C).(\lambda (x2: T).(\lambda (x3: T).(\lambda (H21: (eq C e
-(CHead x1 x0 x2))).(\lambda (H22: (drop n0 O c0 (CHead x1 x0 x3))).(\lambda
-(H23: (subst0 (minus i0 (s x0 n0)) v x2 x3)).(eq_ind_r C (CHead x1 x0 x2)
-(\lambda (c: C).(or4 (drop (S n0) O (CHead c0 (Bind b) t) c) (ex3_4 K C T T
-(\lambda (k: K).(\lambda (e0: C).(\lambda (u0: T).(\lambda (_: T).(eq C c
-(CHead e0 k u0)))))) (\lambda (k: K).(\lambda (e0: C).(\lambda (_:
-T).(\lambda (w: T).(drop (S n0) O (CHead c0 (Bind b) t) (CHead e0 k w))))))
-(\lambda (k: K).(\lambda (_: C).(\lambda (u0: T).(\lambda (w: T).(subst0
-(minus (s (Bind b) i0) (s k (S n0))) v u0 w)))))) (ex3_4 K C C T (\lambda (k:
-K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u0: T).(eq C c (CHead e1 k
-u0)))))) (\lambda (k: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (u0:
-T).(drop (S n0) O (CHead c0 (Bind b) t) (CHead e2 k u0)))))) (\lambda (k:
-K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (minus (s (Bind
-b) i0) (s k (S n0))) v e1 e2)))))) (ex4_5 K C C T T (\lambda (k: K).(\lambda
-(e1: C).(\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(eq C c (CHead e1 k
-u0))))))) (\lambda (k: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (_:
-T).(\lambda (w: T).(drop (S n0) O (CHead c0 (Bind b) t) (CHead e2 k w)))))))
-(\lambda (k: K).(\lambda (_: C).(\lambda (_: C).(\lambda (u0: T).(\lambda (w:
-T).(subst0 (minus (s (Bind b) i0) (s k (S n0))) v u0 w)))))) (\lambda (k:
-K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0
-(minus (s (Bind b) i0) (s k (S n0))) v e1 e2))))))))) (or4_intro1 (drop (S
-n0) O (CHead c0 (Bind b) t) (CHead x1 x0 x2)) (ex3_4 K C T T (\lambda (k:
-K).(\lambda (e0: C).(\lambda (u0: T).(\lambda (_: T).(eq C (CHead x1 x0 x2)
-(CHead e0 k u0)))))) (\lambda (k: K).(\lambda (e0: C).(\lambda (_:
-T).(\lambda (w: T).(drop (S n0) O (CHead c0 (Bind b) t) (CHead e0 k w))))))
-(\lambda (k: K).(\lambda (_: C).(\lambda (u0: T).(\lambda (w: T).(subst0
-(minus (s (Bind b) i0) (s k (S n0))) v u0 w)))))) (ex3_4 K C C T (\lambda (k:
-K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u0: T).(eq C (CHead x1 x0 x2)
-(CHead e1 k u0)))))) (\lambda (k: K).(\lambda (_: C).(\lambda (e2:
-C).(\lambda (u0: T).(drop (S n0) O (CHead c0 (Bind b) t) (CHead e2 k u0))))))
-(\lambda (k: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0
-(minus (s (Bind b) i0) (s k (S n0))) v e1 e2)))))) (ex4_5 K C C T T (\lambda
-(k: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(eq
-C (CHead x1 x0 x2) (CHead e1 k u0))))))) (\lambda (k: K).(\lambda (_:
-C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead c0
-(Bind b) t) (CHead e2 k w))))))) (\lambda (k: K).(\lambda (_: C).(\lambda (_:
-C).(\lambda (u0: T).(\lambda (w: T).(subst0 (minus (s (Bind b) i0) (s k (S
-n0))) v u0 w)))))) (\lambda (k: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda
-(_: T).(\lambda (_: T).(csubst0 (minus (s (Bind b) i0) (s k (S n0))) v e1
-e2))))))) (ex3_4_intro K C T T (\lambda (k: K).(\lambda (e0: C).(\lambda (u0:
-T).(\lambda (_: T).(eq C (CHead x1 x0 x2) (CHead e0 k u0)))))) (\lambda (k:
-K).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead c0
-(Bind b) t) (CHead e0 k w)))))) (\lambda (k: K).(\lambda (_: C).(\lambda (u0:
-T).(\lambda (w: T).(subst0 (minus (s (Bind b) i0) (s k (S n0))) v u0 w)))))
-x0 x1 x2 x3 (refl_equal C (CHead x1 x0 x2)) (drop_drop (Bind b) n0 c0 (CHead
-x1 x0 x3) H22 t) (eq_ind_r nat (S (s x0 n0)) (\lambda (n: nat).(subst0 (minus
-(s (Bind b) i0) n) v x2 x3)) H23 (s x0 (S n0)) (s_S x0 n0)))) e H21))))))))
-H20)) (\lambda (H20: (ex3_4 K C C T (\lambda (k: K).(\lambda (e1: C).(\lambda
-(_: C).(\lambda (u: T).(eq C e (CHead e1 k u)))))) (\lambda (k: K).(\lambda
-(_: C).(\lambda (e2: C).(\lambda (u: T).(drop n0 O c0 (CHead e2 k u))))))
-(\lambda (k: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0
-(minus i0 (s k n0)) v e1 e2))))))).(ex3_4_ind K C C T (\lambda (k:
-K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u0: T).(eq C e (CHead e1 k
-u0)))))) (\lambda (k: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (u0:
-T).(drop n0 O c0 (CHead e2 k u0)))))) (\lambda (k: K).(\lambda (e1:
-C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (minus i0 (s k n0)) v e1 e2)))))
-(or4 (drop (S n0) O (CHead c0 (Bind b) t) e) (ex3_4 K C T T (\lambda (k:
-K).(\lambda (e0: C).(\lambda (u0: T).(\lambda (_: T).(eq C e (CHead e0 k
-u0)))))) (\lambda (k: K).(\lambda (e0: C).(\lambda (_: T).(\lambda (w:
-T).(drop (S n0) O (CHead c0 (Bind b) t) (CHead e0 k w)))))) (\lambda (k: