+f) x1) (s k0 (S n0))) v e1 e2)))))) (ex4_5 K C C T T (\lambda (k0:
+K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq C e
+(CHead e1 k0 u))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead x0 (Flat f) t)
+(CHead e2 k0 w))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus (s (Flat f) x1) (s k0 (S
+n0))) v u w)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda
+(_: T).(\lambda (_: T).(csubst0 (minus (s (Flat f) x1) (s k0 (S n0))) v e1
+e2)))))))) (\lambda (x2: K).(\lambda (x3: C).(\lambda (x4: C).(\lambda (x5:
+T).(\lambda (x6: T).(\lambda (H14: (eq C e (CHead x3 x2 x5))).(\lambda (H15:
+(drop (S n0) O x0 (CHead x4 x2 x6))).(\lambda (H16: (subst0 (minus x1 (s x2
+(S n0))) v x5 x6)).(\lambda (H17: (csubst0 (minus x1 (s x2 (S n0))) v x3
+x4)).(eq_ind_r C (CHead x3 x2 x5) (\lambda (c0: C).(or4 (drop (S n0) O (CHead
+x0 (Flat f) t) c0) (ex3_4 K C T T (\lambda (k0: K).(\lambda (e0: C).(\lambda
+(u: T).(\lambda (_: T).(eq C c0 (CHead e0 k0 u)))))) (\lambda (k0:
+K).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead x0
+(Flat f) t) (CHead e0 k0 w)))))) (\lambda (k0: K).(\lambda (_: C).(\lambda
+(u: T).(\lambda (w: T).(subst0 (minus (s (Flat f) x1) (s k0 (S n0))) v u
+w)))))) (ex3_4 K C C T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u: T).(eq C c0 (CHead e1 k0 u)))))) (\lambda (k0: K).(\lambda
+(_: C).(\lambda (e2: C).(\lambda (u: T).(drop (S n0) O (CHead x0 (Flat f) t)
+(CHead e2 k0 u)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda (e2:
+C).(\lambda (_: T).(csubst0 (minus (s (Flat f) x1) (s k0 (S n0))) v e1
+e2)))))) (ex4_5 K C C T T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (_: T).(eq C c0 (CHead e1 k0 u))))))) (\lambda
+(k0: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w:
+T).(drop (S n0) O (CHead x0 (Flat f) t) (CHead e2 k0 w))))))) (\lambda (k0:
+K).(\lambda (_: C).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0
+(minus (s (Flat f) x1) (s k0 (S n0))) v u w)))))) (\lambda (k0: K).(\lambda
+(e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus (s
+(Flat f) x1) (s k0 (S n0))) v e1 e2))))))))) (or4_intro3 (drop (S n0) O
+(CHead x0 (Flat f) t) (CHead x3 x2 x5)) (ex3_4 K C T T (\lambda (k0:
+K).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C (CHead x3 x2 x5)
+(CHead e0 k0 u)))))) (\lambda (k0: K).(\lambda (e0: C).(\lambda (_:
+T).(\lambda (w: T).(drop (S n0) O (CHead x0 (Flat f) t) (CHead e0 k0 w))))))
+(\lambda (k0: K).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0
+(minus (s (Flat f) x1) (s k0 (S n0))) v u w)))))) (ex3_4 K C C T (\lambda
+(k0: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(eq C (CHead x3 x2
+x5) (CHead e1 k0 u)))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (u: T).(drop (S n0) O (CHead x0 (Flat f) t) (CHead e2 k0 u))))))
+(\lambda (k0: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0
+(minus (s (Flat f) x1) (s k0 (S n0))) v e1 e2)))))) (ex4_5 K C C T T (\lambda
+(k0: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq
+C (CHead x3 x2 x5) (CHead e1 k0 u))))))) (\lambda (k0: K).(\lambda (_:
+C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead x0
+(Flat f) t) (CHead e2 k0 w))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda
+(_: C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus (s (Flat f) x1) (s k0
+(S n0))) v u w)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda (e2:
+C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus (s (Flat f) x1) (s k0 (S
+n0))) v e1 e2))))))) (ex4_5_intro K C C T T (\lambda (k0: K).(\lambda (e1:
+C).(\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq C (CHead x3 x2 x5)
+(CHead e1 k0 u))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead x0 (Flat f) t)
+(CHead e2 k0 w))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus (s (Flat f) x1) (s k0 (S
+n0))) v u w)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda
+(_: T).(\lambda (_: T).(csubst0 (minus (s (Flat f) x1) (s k0 (S n0))) v e1
+e2)))))) x2 x3 x4 x5 x6 (refl_equal C (CHead x3 x2 x5)) (drop_drop (Flat f)
+n0 x0 (CHead x4 x2 x6) H15 t) H16 H17)) e H14)))))))))) H13)) H12)))))) k
+(drop_gen_drop k c e t n0 H2) H7 H8) i H4))) c2 H5)))))) H3)) (\lambda (H3:
+(ex4_3 T C nat (\lambda (_: T).(\lambda (_: C).(\lambda (j: nat).(eq nat i (s
+k j))))) (\lambda (u2: T).(\lambda (c3: C).(\lambda (_: nat).(eq C c2 (CHead
+c3 k u2))))) (\lambda (u2: T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v t
+u2)))) (\lambda (_: T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c
+c3)))))).(ex4_3_ind T C nat (\lambda (_: T).(\lambda (_: C).(\lambda (j:
+nat).(eq nat i (s k j))))) (\lambda (u2: T).(\lambda (c3: C).(\lambda (_:
+nat).(eq C c2 (CHead c3 k u2))))) (\lambda (u2: T).(\lambda (_: C).(\lambda
+(j: nat).(subst0 j v t u2)))) (\lambda (_: T).(\lambda (c3: C).(\lambda (j:
+nat).(csubst0 j v c c3)))) (or4 (drop (S n0) O c2 e) (ex3_4 K C T T (\lambda
+(k0: K).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C e (CHead e0 k0
+u)))))) (\lambda (k0: K).(\lambda (e0: C).(\lambda (_: T).(\lambda (w:
+T).(drop (S n0) O c2 (CHead e0 k0 w)))))) (\lambda (k0: K).(\lambda (_:
+C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus i (s k0 (S n0))) v u
+w)))))) (ex3_4 K C C T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u: T).(eq C e (CHead e1 k0 u)))))) (\lambda (k0: K).(\lambda (_:
+C).(\lambda (e2: C).(\lambda (u: T).(drop (S n0) O c2 (CHead e2 k0 u))))))
+(\lambda (k0: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0
+(minus i (s k0 (S n0))) v e1 e2)))))) (ex4_5 K C C T T (\lambda (k0:
+K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq C e
+(CHead e1 k0 u))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O c2 (CHead e2 k0 w)))))))
+(\lambda (k0: K).(\lambda (_: C).(\lambda (_: C).(\lambda (u: T).(\lambda (w:
+T).(subst0 (minus i (s k0 (S n0))) v u w)))))) (\lambda (k0: K).(\lambda (e1:
+C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus i (s k0
+(S n0))) v e1 e2)))))))) (\lambda (x0: T).(\lambda (x1: C).(\lambda (x2:
+nat).(\lambda (H4: (eq nat i (s k x2))).(\lambda (H5: (eq C c2 (CHead x1 k
+x0))).(\lambda (_: (subst0 x2 v t x0)).(\lambda (H7: (csubst0 x2 v c
+x1)).(eq_ind_r C (CHead x1 k x0) (\lambda (c0: C).(or4 (drop (S n0) O c0 e)
+(ex3_4 K C T T (\lambda (k0: K).(\lambda (e0: C).(\lambda (u: T).(\lambda (_:
+T).(eq C e (CHead e0 k0 u)))))) (\lambda (k0: K).(\lambda (e0: C).(\lambda
+(_: T).(\lambda (w: T).(drop (S n0) O c0 (CHead e0 k0 w)))))) (\lambda (k0:
+K).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus i (s k0 (S
+n0))) v u w)))))) (ex3_4 K C C T (\lambda (k0: K).(\lambda (e1: C).(\lambda
+(_: C).(\lambda (u: T).(eq C e (CHead e1 k0 u)))))) (\lambda (k0: K).(\lambda
+(_: C).(\lambda (e2: C).(\lambda (u: T).(drop (S n0) O c0 (CHead e2 k0
+u)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
+T).(csubst0 (minus i (s k0 (S n0))) v e1 e2)))))) (ex4_5 K C C T T (\lambda
+(k0: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq
+C e (CHead e1 k0 u))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O c0 (CHead e2 k0 w)))))))
+(\lambda (k0: K).(\lambda (_: C).(\lambda (_: C).(\lambda (u: T).(\lambda (w:
+T).(subst0 (minus i (s k0 (S n0))) v u w)))))) (\lambda (k0: K).(\lambda (e1:
+C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus i (s k0
+(S n0))) v e1 e2))))))))) (let H8 \def (eq_ind nat i (\lambda (n1:
+nat).(\forall (c3: C).(\forall (v0: T).((csubst0 n1 v0 c c3) \to (\forall
+(e0: C).((drop (S n0) O c e0) \to (or4 (drop (S n0) O c3 e0) (ex3_4 K C T T
+(\lambda (k0: K).(\lambda (e1: C).(\lambda (u: T).(\lambda (_: T).(eq C e0
+(CHead e1 k0 u)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda (_:
+T).(\lambda (w: T).(drop (S n0) O c3 (CHead e1 k0 w)))))) (\lambda (k0:
+K).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus n1 (s k0 (S
+n0))) v0 u w)))))) (ex3_4 K C C T (\lambda (k0: K).(\lambda (e1: C).(\lambda
+(_: C).(\lambda (u: T).(eq C e0 (CHead e1 k0 u)))))) (\lambda (k0:
+K).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(drop (S n0) O c3 (CHead
+e2 k0 u)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
+T).(csubst0 (minus n1 (s k0 (S n0))) v0 e1 e2)))))) (ex4_5 K C C T T (\lambda
+(k0: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq
+C e0 (CHead e1 k0 u))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O c3 (CHead e2 k0 w)))))))
+(\lambda (k0: K).(\lambda (_: C).(\lambda (_: C).(\lambda (u: T).(\lambda (w:
+T).(subst0 (minus n1 (s k0 (S n0))) v0 u w)))))) (\lambda (k0: K).(\lambda
+(e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus n1
+(s k0 (S n0))) v0 e1 e2)))))))))))))) H0 (s k x2) H4) in (let H9 \def (eq_ind
+nat i (\lambda (n1: nat).(lt (S n0) n1)) H (s k x2) H4) in (eq_ind_r nat (s k
+x2) (\lambda (n1: nat).(or4 (drop (S n0) O (CHead x1 k x0) e) (ex3_4 K C T T
+(\lambda (k0: K).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C e
+(CHead e0 k0 u)))))) (\lambda (k0: K).(\lambda (e0: C).(\lambda (_:
+T).(\lambda (w: T).(drop (S n0) O (CHead x1 k x0) (CHead e0 k0 w))))))
+(\lambda (k0: K).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0
+(minus n1 (s k0 (S n0))) v u w)))))) (ex3_4 K C C T (\lambda (k0: K).(\lambda
+(e1: C).(\lambda (_: C).(\lambda (u: T).(eq C e (CHead e1 k0 u)))))) (\lambda
+(k0: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(drop (S n0) O
+(CHead x1 k x0) (CHead e2 k0 u)))))) (\lambda (k0: K).(\lambda (e1:
+C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (minus n1 (s k0 (S n0))) v e1
+e2)))))) (ex4_5 K C C T T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (_: T).(eq C e (CHead e1 k0 u))))))) (\lambda
+(k0: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w:
+T).(drop (S n0) O (CHead x1 k x0) (CHead e2 k0 w))))))) (\lambda (k0:
+K).(\lambda (_: C).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0
+(minus n1 (s k0 (S n0))) v u w)))))) (\lambda (k0: K).(\lambda (e1:
+C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus n1 (s k0
+(S n0))) v e1 e2))))))))) (K_ind (\lambda (k0: K).((drop (r k0 n0) O c e) \to
+(((\forall (c3: C).(\forall (v0: T).((csubst0 (s k0 x2) v0 c c3) \to (\forall
+(e0: C).((drop (S n0) O c e0) \to (or4 (drop (S n0) O c3 e0) (ex3_4 K C T T
+(\lambda (k1: K).(\lambda (e1: C).(\lambda (u: T).(\lambda (_: T).(eq C e0
+(CHead e1 k1 u)))))) (\lambda (k1: K).(\lambda (e1: C).(\lambda (_:
+T).(\lambda (w: T).(drop (S n0) O c3 (CHead e1 k1 w)))))) (\lambda (k1:
+K).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus (s k0 x2)
+(s k1 (S n0))) v0 u w)))))) (ex3_4 K C C T (\lambda (k1: K).(\lambda (e1:
+C).(\lambda (_: C).(\lambda (u: T).(eq C e0 (CHead e1 k1 u)))))) (\lambda
+(k1: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(drop (S n0) O c3
+(CHead e2 k1 u)))))) (\lambda (k1: K).(\lambda (e1: C).(\lambda (e2:
+C).(\lambda (_: T).(csubst0 (minus (s k0 x2) (s k1 (S n0))) v0 e1 e2))))))
+(ex4_5 K C C T T (\lambda (k1: K).(\lambda (e1: C).(\lambda (_: C).(\lambda
+(u: T).(\lambda (_: T).(eq C e0 (CHead e1 k1 u))))))) (\lambda (k1:
+K).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(drop (S
+n0) O c3 (CHead e2 k1 w))))))) (\lambda (k1: K).(\lambda (_: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus (s k0 x2) (s k1 (S n0))) v0
+u w)))))) (\lambda (k1: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
+T).(\lambda (_: T).(csubst0 (minus (s k0 x2) (s k1 (S n0))) v0 e1
+e2)))))))))))))) \to ((lt (S n0) (s k0 x2)) \to (or4 (drop (S n0) O (CHead x1
+k0 x0) e) (ex3_4 K C T T (\lambda (k1: K).(\lambda (e0: C).(\lambda (u:
+T).(\lambda (_: T).(eq C e (CHead e0 k1 u)))))) (\lambda (k1: K).(\lambda
+(e0: C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead x1 k0 x0)
+(CHead e0 k1 w)))))) (\lambda (k1: K).(\lambda (_: C).(\lambda (u:
+T).(\lambda (w: T).(subst0 (minus (s k0 x2) (s k1 (S n0))) v u w)))))) (ex3_4
+K C C T (\lambda (k1: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(eq
+C e (CHead e1 k1 u)))))) (\lambda (k1: K).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (u: T).(drop (S n0) O (CHead x1 k0 x0) (CHead e2 k1 u))))))
+(\lambda (k1: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0
+(minus (s k0 x2) (s k1 (S n0))) v e1 e2)))))) (ex4_5 K C C T T (\lambda (k1:
+K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq C e
+(CHead e1 k1 u))))))) (\lambda (k1: K).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead x1 k0 x0) (CHead e2
+k1 w))))))) (\lambda (k1: K).(\lambda (_: C).(\lambda (_: C).(\lambda (u:
+T).(\lambda (w: T).(subst0 (minus (s k0 x2) (s k1 (S n0))) v u w))))))
+(\lambda (k1: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
+(_: T).(csubst0 (minus (s k0 x2) (s k1 (S n0))) v e1 e2)))))))))))) (\lambda
+(b: B).(\lambda (H10: (drop (r (Bind b) n0) O c e)).(\lambda (_: ((\forall
+(c3: C).(\forall (v0: T).((csubst0 (s (Bind b) x2) v0 c c3) \to (\forall (e0:
+C).((drop (S n0) O c e0) \to (or4 (drop (S n0) O c3 e0) (ex3_4 K C T T
+(\lambda (k0: K).(\lambda (e1: C).(\lambda (u: T).(\lambda (_: T).(eq C e0
+(CHead e1 k0 u)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda (_:
+T).(\lambda (w: T).(drop (S n0) O c3 (CHead e1 k0 w)))))) (\lambda (k0:
+K).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus (s (Bind b)
+x2) (s k0 (S n0))) v0 u w)))))) (ex3_4 K C C T (\lambda (k0: K).(\lambda (e1:
+C).(\lambda (_: C).(\lambda (u: T).(eq C e0 (CHead e1 k0 u)))))) (\lambda
+(k0: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(drop (S n0) O c3
+(CHead e2 k0 u)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda (e2:
+C).(\lambda (_: T).(csubst0 (minus (s (Bind b) x2) (s k0 (S n0))) v0 e1
+e2)))))) (ex4_5 K C C T T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (_: T).(eq C e0 (CHead e1 k0 u))))))) (\lambda
+(k0: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w:
+T).(drop (S n0) O c3 (CHead e2 k0 w))))))) (\lambda (k0: K).(\lambda (_:
+C).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus (s (Bind b)
+x2) (s k0 (S n0))) v0 u w)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda
+(e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus (s (Bind b) x2) (s k0
+(S n0))) v0 e1 e2))))))))))))))).(\lambda (H12: (lt (S n0) (s (Bind b)
+x2))).(let H13 \def (IHn x2 (le_S_n (S n0) x2 H12) c x1 v H7 e H10) in
+(or4_ind (drop n0 O x1 e) (ex3_4 K C T T (\lambda (k0: K).(\lambda (e0:
+C).(\lambda (u: T).(\lambda (_: T).(eq C e (CHead e0 k0 u)))))) (\lambda (k0:
+K).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(drop n0 O x1 (CHead e0
+k0 w)))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (u: T).(\lambda (w:
+T).(subst0 (minus x2 (s k0 n0)) v u w)))))) (ex3_4 K C C T (\lambda (k0:
+K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(eq C e (CHead e1 k0
+u)))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (u:
+T).(drop n0 O x1 (CHead e2 k0 u)))))) (\lambda (k0: K).(\lambda (e1:
+C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (minus x2 (s k0 n0)) v e1
+e2)))))) (ex4_5 K C C T T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (_: T).(eq C e (CHead e1 k0 u))))))) (\lambda
+(k0: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w:
+T).(drop n0 O x1 (CHead e2 k0 w))))))) (\lambda (k0: K).(\lambda (_:
+C).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus x2 (s k0
+n0)) v u w)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda
+(_: T).(\lambda (_: T).(csubst0 (minus x2 (s k0 n0)) v e1 e2))))))) (or4
+(drop (S n0) O (CHead x1 (Bind b) x0) e) (ex3_4 K C T T (\lambda (k0:
+K).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C e (CHead e0 k0
+u)))))) (\lambda (k0: K).(\lambda (e0: C).(\lambda (_: T).(\lambda (w:
+T).(drop (S n0) O (CHead x1 (Bind b) x0) (CHead e0 k0 w)))))) (\lambda (k0:
+K).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus (s (Bind b)
+x2) (s k0 (S n0))) v u w)))))) (ex3_4 K C C T (\lambda (k0: K).(\lambda (e1:
+C).(\lambda (_: C).(\lambda (u: T).(eq C e (CHead e1 k0 u)))))) (\lambda (k0:
+K).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(drop (S n0) O (CHead x1
+(Bind b) x0) (CHead e2 k0 u)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda
+(e2: C).(\lambda (_: T).(csubst0 (minus (s (Bind b) x2) (s k0 (S n0))) v e1
+e2)))))) (ex4_5 K C C T T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (_: T).(eq C e (CHead e1 k0 u))))))) (\lambda
+(k0: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w:
+T).(drop (S n0) O (CHead x1 (Bind b) x0) (CHead e2 k0 w))))))) (\lambda (k0:
+K).(\lambda (_: C).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0
+(minus (s (Bind b) x2) (s k0 (S n0))) v u w)))))) (\lambda (k0: K).(\lambda
+(e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus (s
+(Bind b) x2) (s k0 (S n0))) v e1 e2)))))))) (\lambda (H14: (drop n0 O x1
+e)).(or4_intro0 (drop (S n0) O (CHead x1 (Bind b) x0) e) (ex3_4 K C T T
+(\lambda (k0: K).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C e
+(CHead e0 k0 u)))))) (\lambda (k0: K).(\lambda (e0: C).(\lambda (_:
+T).(\lambda (w: T).(drop (S n0) O (CHead x1 (Bind b) x0) (CHead e0 k0 w))))))
+(\lambda (k0: K).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0
+(minus (s (Bind b) x2) (s k0 (S n0))) v u w)))))) (ex3_4 K C C T (\lambda
+(k0: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(eq C e (CHead e1 k0
+u)))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (u:
+T).(drop (S n0) O (CHead x1 (Bind b) x0) (CHead e2 k0 u)))))) (\lambda (k0:
+K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (minus (s (Bind
+b) x2) (s k0 (S n0))) v e1 e2)))))) (ex4_5 K C C T T (\lambda (k0:
+K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq C e
+(CHead e1 k0 u))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead x1 (Bind b) x0)
+(CHead e2 k0 w))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus (s (Bind b) x2) (s k0 (S
+n0))) v u w)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda
+(_: T).(\lambda (_: T).(csubst0 (minus (s (Bind b) x2) (s k0 (S n0))) v e1
+e2))))))) (drop_drop (Bind b) n0 x1 e H14 x0))) (\lambda (H14: (ex3_4 K C T T
+(\lambda (k0: K).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C e
+(CHead e0 k0 u)))))) (\lambda (k0: K).(\lambda (e0: C).(\lambda (_:
+T).(\lambda (w: T).(drop n0 O x1 (CHead e0 k0 w)))))) (\lambda (k0:
+K).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus x2 (s k0
+n0)) v u w))))))).(ex3_4_ind K C T T (\lambda (k0: K).(\lambda (e0:
+C).(\lambda (u: T).(\lambda (_: T).(eq C e (CHead e0 k0 u)))))) (\lambda (k0:
+K).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(drop n0 O x1 (CHead e0
+k0 w)))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (u: T).(\lambda (w:
+T).(subst0 (minus x2 (s k0 n0)) v u w))))) (or4 (drop (S n0) O (CHead x1
+(Bind b) x0) e) (ex3_4 K C T T (\lambda (k0: K).(\lambda (e0: C).(\lambda (u:
+T).(\lambda (_: T).(eq C e (CHead e0 k0 u)))))) (\lambda (k0: K).(\lambda
+(e0: C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead x1 (Bind b) x0)
+(CHead e0 k0 w)))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (u:
+T).(\lambda (w: T).(subst0 (minus (s (Bind b) x2) (s k0 (S n0))) v u w))))))
+(ex3_4 K C C T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u:
+T).(eq C e (CHead e1 k0 u)))))) (\lambda (k0: K).(\lambda (_: C).(\lambda
+(e2: C).(\lambda (u: T).(drop (S n0) O (CHead x1 (Bind b) x0) (CHead e2 k0
+u)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
+T).(csubst0 (minus (s (Bind b) x2) (s k0 (S n0))) v e1 e2)))))) (ex4_5 K C C
+T T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u:
+T).(\lambda (_: T).(eq C e (CHead e1 k0 u))))))) (\lambda (k0: K).(\lambda
+(_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead
+x1 (Bind b) x0) (CHead e2 k0 w))))))) (\lambda (k0: K).(\lambda (_:
+C).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus (s (Bind b)
+x2) (s k0 (S n0))) v u w)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda
+(e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus (s (Bind b) x2) (s k0
+(S n0))) v e1 e2)))))))) (\lambda (x3: K).(\lambda (x4: C).(\lambda (x5:
+T).(\lambda (x6: T).(\lambda (H15: (eq C e (CHead x4 x3 x5))).(\lambda (H16:
+(drop n0 O x1 (CHead x4 x3 x6))).(\lambda (H17: (subst0 (minus x2 (s x3 n0))
+v x5 x6)).(eq_ind_r C (CHead x4 x3 x5) (\lambda (c0: C).(or4 (drop (S n0) O
+(CHead x1 (Bind b) x0) c0) (ex3_4 K C T T (\lambda (k0: K).(\lambda (e0:
+C).(\lambda (u: T).(\lambda (_: T).(eq C c0 (CHead e0 k0 u)))))) (\lambda
+(k0: K).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O
+(CHead x1 (Bind b) x0) (CHead e0 k0 w)))))) (\lambda (k0: K).(\lambda (_:
+C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus (s (Bind b) x2) (s k0 (S
+n0))) v u w)))))) (ex3_4 K C C T (\lambda (k0: K).(\lambda (e1: C).(\lambda
+(_: C).(\lambda (u: T).(eq C c0 (CHead e1 k0 u)))))) (\lambda (k0:
+K).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(drop (S n0) O (CHead x1
+(Bind b) x0) (CHead e2 k0 u)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda
+(e2: C).(\lambda (_: T).(csubst0 (minus (s (Bind b) x2) (s k0 (S n0))) v e1
+e2)))))) (ex4_5 K C C T T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (_: T).(eq C c0 (CHead e1 k0 u))))))) (\lambda
+(k0: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w:
+T).(drop (S n0) O (CHead x1 (Bind b) x0) (CHead e2 k0 w))))))) (\lambda (k0:
+K).(\lambda (_: C).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0
+(minus (s (Bind b) x2) (s k0 (S n0))) v u w)))))) (\lambda (k0: K).(\lambda
+(e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus (s
+(Bind b) x2) (s k0 (S n0))) v e1 e2))))))))) (or4_intro1 (drop (S n0) O
+(CHead x1 (Bind b) x0) (CHead x4 x3 x5)) (ex3_4 K C T T (\lambda (k0:
+K).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C (CHead x4 x3 x5)
+(CHead e0 k0 u)))))) (\lambda (k0: K).(\lambda (e0: C).(\lambda (_:
+T).(\lambda (w: T).(drop (S n0) O (CHead x1 (Bind b) x0) (CHead e0 k0 w))))))
+(\lambda (k0: K).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0
+(minus (s (Bind b) x2) (s k0 (S n0))) v u w)))))) (ex3_4 K C C T (\lambda
+(k0: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(eq C (CHead x4 x3
+x5) (CHead e1 k0 u)))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (u: T).(drop (S n0) O (CHead x1 (Bind b) x0) (CHead e2 k0 u))))))
+(\lambda (k0: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0
+(minus (s (Bind b) x2) (s k0 (S n0))) v e1 e2)))))) (ex4_5 K C C T T (\lambda
+(k0: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq
+C (CHead x4 x3 x5) (CHead e1 k0 u))))))) (\lambda (k0: K).(\lambda (_:
+C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead x1
+(Bind b) x0) (CHead e2 k0 w))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda
+(_: C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus (s (Bind b) x2) (s k0
+(S n0))) v u w)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda (e2:
+C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus (s (Bind b) x2) (s k0 (S
+n0))) v e1 e2))))))) (ex3_4_intro K C T T (\lambda (k0: K).(\lambda (e0:
+C).(\lambda (u: T).(\lambda (_: T).(eq C (CHead x4 x3 x5) (CHead e0 k0
+u)))))) (\lambda (k0: K).(\lambda (e0: C).(\lambda (_: T).(\lambda (w:
+T).(drop (S n0) O (CHead x1 (Bind b) x0) (CHead e0 k0 w)))))) (\lambda (k0:
+K).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus (s (Bind b)
+x2) (s k0 (S n0))) v u w))))) x3 x4 x5 x6 (refl_equal C (CHead x4 x3 x5))
+(drop_drop (Bind b) n0 x1 (CHead x4 x3 x6) H16 x0) (eq_ind_r nat (S (s x3
+n0)) (\lambda (n1: nat).(subst0 (minus (s (Bind b) x2) n1) v x5 x6)) H17 (s
+x3 (S n0)) (s_S x3 n0)))) e H15)))))))) H14)) (\lambda (H14: (ex3_4 K C C T
+(\lambda (k0: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(eq C e
+(CHead e1 k0 u)))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (u: T).(drop n0 O x1 (CHead e2 k0 u)))))) (\lambda (k0:
+K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (minus x2 (s k0
+n0)) v e1 e2))))))).(ex3_4_ind K C C T (\lambda (k0: K).(\lambda (e1:
+C).(\lambda (_: C).(\lambda (u: T).(eq C e (CHead e1 k0 u)))))) (\lambda (k0:
+K).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(drop n0 O x1 (CHead e2
+k0 u)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
+T).(csubst0 (minus x2 (s k0 n0)) v e1 e2))))) (or4 (drop (S n0) O (CHead x1
+(Bind b) x0) e) (ex3_4 K C T T (\lambda (k0: K).(\lambda (e0: C).(\lambda (u:
+T).(\lambda (_: T).(eq C e (CHead e0 k0 u)))))) (\lambda (k0: K).(\lambda
+(e0: C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead x1 (Bind b) x0)
+(CHead e0 k0 w)))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (u:
+T).(\lambda (w: T).(subst0 (minus (s (Bind b) x2) (s k0 (S n0))) v u w))))))
+(ex3_4 K C C T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u:
+T).(eq C e (CHead e1 k0 u)))))) (\lambda (k0: K).(\lambda (_: C).(\lambda
+(e2: C).(\lambda (u: T).(drop (S n0) O (CHead x1 (Bind b) x0) (CHead e2 k0
+u)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
+T).(csubst0 (minus (s (Bind b) x2) (s k0 (S n0))) v e1 e2)))))) (ex4_5 K C C
+T T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u:
+T).(\lambda (_: T).(eq C e (CHead e1 k0 u))))))) (\lambda (k0: K).(\lambda
+(_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead
+x1 (Bind b) x0) (CHead e2 k0 w))))))) (\lambda (k0: K).(\lambda (_:
+C).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus (s (Bind b)
+x2) (s k0 (S n0))) v u w)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda
+(e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus (s (Bind b) x2) (s k0
+(S n0))) v e1 e2)))))))) (\lambda (x3: K).(\lambda (x4: C).(\lambda (x5:
+C).(\lambda (x6: T).(\lambda (H15: (eq C e (CHead x4 x3 x6))).(\lambda (H16:
+(drop n0 O x1 (CHead x5 x3 x6))).(\lambda (H17: (csubst0 (minus x2 (s x3 n0))
+v x4 x5)).(eq_ind_r C (CHead x4 x3 x6) (\lambda (c0: C).(or4 (drop (S n0) O
+(CHead x1 (Bind b) x0) c0) (ex3_4 K C T T (\lambda (k0: K).(\lambda (e0:
+C).(\lambda (u: T).(\lambda (_: T).(eq C c0 (CHead e0 k0 u)))))) (\lambda
+(k0: K).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O
+(CHead x1 (Bind b) x0) (CHead e0 k0 w)))))) (\lambda (k0: K).(\lambda (_:
+C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus (s (Bind b) x2) (s k0 (S
+n0))) v u w)))))) (ex3_4 K C C T (\lambda (k0: K).(\lambda (e1: C).(\lambda
+(_: C).(\lambda (u: T).(eq C c0 (CHead e1 k0 u)))))) (\lambda (k0:
+K).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(drop (S n0) O (CHead x1
+(Bind b) x0) (CHead e2 k0 u)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda
+(e2: C).(\lambda (_: T).(csubst0 (minus (s (Bind b) x2) (s k0 (S n0))) v e1
+e2)))))) (ex4_5 K C C T T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (_: T).(eq C c0 (CHead e1 k0 u))))))) (\lambda
+(k0: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w:
+T).(drop (S n0) O (CHead x1 (Bind b) x0) (CHead e2 k0 w))))))) (\lambda (k0:
+K).(\lambda (_: C).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0
+(minus (s (Bind b) x2) (s k0 (S n0))) v u w)))))) (\lambda (k0: K).(\lambda
+(e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus (s
+(Bind b) x2) (s k0 (S n0))) v e1 e2))))))))) (or4_intro2 (drop (S n0) O
+(CHead x1 (Bind b) x0) (CHead x4 x3 x6)) (ex3_4 K C T T (\lambda (k0:
+K).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C (CHead x4 x3 x6)
+(CHead e0 k0 u)))))) (\lambda (k0: K).(\lambda (e0: C).(\lambda (_:
+T).(\lambda (w: T).(drop (S n0) O (CHead x1 (Bind b) x0) (CHead e0 k0 w))))))
+(\lambda (k0: K).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0
+(minus (s (Bind b) x2) (s k0 (S n0))) v u w)))))) (ex3_4 K C C T (\lambda
+(k0: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(eq C (CHead x4 x3
+x6) (CHead e1 k0 u)))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (u: T).(drop (S n0) O (CHead x1 (Bind b) x0) (CHead e2 k0 u))))))
+(\lambda (k0: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0
+(minus (s (Bind b) x2) (s k0 (S n0))) v e1 e2)))))) (ex4_5 K C C T T (\lambda
+(k0: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq
+C (CHead x4 x3 x6) (CHead e1 k0 u))))))) (\lambda (k0: K).(\lambda (_:
+C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead x1
+(Bind b) x0) (CHead e2 k0 w))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda
+(_: C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus (s (Bind b) x2) (s k0
+(S n0))) v u w)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda (e2:
+C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus (s (Bind b) x2) (s k0 (S
+n0))) v e1 e2))))))) (ex3_4_intro K C C T (\lambda (k0: K).(\lambda (e1:
+C).(\lambda (_: C).(\lambda (u: T).(eq C (CHead x4 x3 x6) (CHead e1 k0
+u)))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (u:
+T).(drop (S n0) O (CHead x1 (Bind b) x0) (CHead e2 k0 u)))))) (\lambda (k0:
+K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (minus (s (Bind
+b) x2) (s k0 (S n0))) v e1 e2))))) x3 x4 x5 x6 (refl_equal C (CHead x4 x3
+x6)) (drop_drop (Bind b) n0 x1 (CHead x5 x3 x6) H16 x0) (eq_ind_r nat (S (s
+x3 n0)) (\lambda (n1: nat).(csubst0 (minus (s (Bind b) x2) n1) v x4 x5)) H17
+(s x3 (S n0)) (s_S x3 n0)))) e H15)))))))) H14)) (\lambda (H14: (ex4_5 K C C
+T T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u:
+T).(\lambda (_: T).(eq C e (CHead e1 k0 u))))))) (\lambda (k0: K).(\lambda
+(_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(drop n0 O x1 (CHead
+e2 k0 w))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (_: C).(\lambda (u:
+T).(\lambda (w: T).(subst0 (minus x2 (s k0 n0)) v u w)))))) (\lambda (k0:
+K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0
+(minus x2 (s k0 n0)) v e1 e2)))))))).(ex4_5_ind K C C T T (\lambda (k0:
+K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq C e
+(CHead e1 k0 u))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (_: T).(\lambda (w: T).(drop n0 O x1 (CHead e2 k0 w)))))))
+(\lambda (k0: K).(\lambda (_: C).(\lambda (_: C).(\lambda (u: T).(\lambda (w:
+T).(subst0 (minus x2 (s k0 n0)) v u w)))))) (\lambda (k0: K).(\lambda (e1:
+C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus x2 (s k0
+n0)) v e1 e2)))))) (or4 (drop (S n0) O (CHead x1 (Bind b) x0) e) (ex3_4 K C T
+T (\lambda (k0: K).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C e
+(CHead e0 k0 u)))))) (\lambda (k0: K).(\lambda (e0: C).(\lambda (_:
+T).(\lambda (w: T).(drop (S n0) O (CHead x1 (Bind b) x0) (CHead e0 k0 w))))))
+(\lambda (k0: K).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0
+(minus (s (Bind b) x2) (s k0 (S n0))) v u w)))))) (ex3_4 K C C T (\lambda
+(k0: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(eq C e (CHead e1 k0
+u)))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (u:
+T).(drop (S n0) O (CHead x1 (Bind b) x0) (CHead e2 k0 u)))))) (\lambda (k0:
+K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (minus (s (Bind
+b) x2) (s k0 (S n0))) v e1 e2)))))) (ex4_5 K C C T T (\lambda (k0:
+K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq C e
+(CHead e1 k0 u))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead x1 (Bind b) x0)
+(CHead e2 k0 w))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus (s (Bind b) x2) (s k0 (S
+n0))) v u w)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda
+(_: T).(\lambda (_: T).(csubst0 (minus (s (Bind b) x2) (s k0 (S n0))) v e1
+e2)))))))) (\lambda (x3: K).(\lambda (x4: C).(\lambda (x5: C).(\lambda (x6:
+T).(\lambda (x7: T).(\lambda (H15: (eq C e (CHead x4 x3 x6))).(\lambda (H16:
+(drop n0 O x1 (CHead x5 x3 x7))).(\lambda (H17: (subst0 (minus x2 (s x3 n0))
+v x6 x7)).(\lambda (H18: (csubst0 (minus x2 (s x3 n0)) v x4 x5)).(eq_ind_r C
+(CHead x4 x3 x6) (\lambda (c0: C).(or4 (drop (S n0) O (CHead x1 (Bind b) x0)
+c0) (ex3_4 K C T T (\lambda (k0: K).(\lambda (e0: C).(\lambda (u: T).(\lambda
+(_: T).(eq C c0 (CHead e0 k0 u)))))) (\lambda (k0: K).(\lambda (e0:
+C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead x1 (Bind b) x0)
+(CHead e0 k0 w)))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (u:
+T).(\lambda (w: T).(subst0 (minus (s (Bind b) x2) (s k0 (S n0))) v u w))))))
+(ex3_4 K C C T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u:
+T).(eq C c0 (CHead e1 k0 u)))))) (\lambda (k0: K).(\lambda (_: C).(\lambda
+(e2: C).(\lambda (u: T).(drop (S n0) O (CHead x1 (Bind b) x0) (CHead e2 k0
+u)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
+T).(csubst0 (minus (s (Bind b) x2) (s k0 (S n0))) v e1 e2)))))) (ex4_5 K C C
+T T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u:
+T).(\lambda (_: T).(eq C c0 (CHead e1 k0 u))))))) (\lambda (k0: K).(\lambda
+(_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead
+x1 (Bind b) x0) (CHead e2 k0 w))))))) (\lambda (k0: K).(\lambda (_:
+C).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus (s (Bind b)
+x2) (s k0 (S n0))) v u w)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda
+(e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus (s (Bind b) x2) (s k0
+(S n0))) v e1 e2))))))))) (or4_intro3 (drop (S n0) O (CHead x1 (Bind b) x0)
+(CHead x4 x3 x6)) (ex3_4 K C T T (\lambda (k0: K).(\lambda (e0: C).(\lambda
+(u: T).(\lambda (_: T).(eq C (CHead x4 x3 x6) (CHead e0 k0 u)))))) (\lambda
+(k0: K).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O
+(CHead x1 (Bind b) x0) (CHead e0 k0 w)))))) (\lambda (k0: K).(\lambda (_:
+C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus (s (Bind b) x2) (s k0 (S
+n0))) v u w)))))) (ex3_4 K C C T (\lambda (k0: K).(\lambda (e1: C).(\lambda
+(_: C).(\lambda (u: T).(eq C (CHead x4 x3 x6) (CHead e1 k0 u)))))) (\lambda
+(k0: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(drop (S n0) O
+(CHead x1 (Bind b) x0) (CHead e2 k0 u)))))) (\lambda (k0: K).(\lambda (e1:
+C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (minus (s (Bind b) x2) (s k0 (S
+n0))) v e1 e2)))))) (ex4_5 K C C T T (\lambda (k0: K).(\lambda (e1:
+C).(\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq C (CHead x4 x3 x6)
+(CHead e1 k0 u))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead x1 (Bind b) x0)
+(CHead e2 k0 w))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus (s (Bind b) x2) (s k0 (S
+n0))) v u w)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda
+(_: T).(\lambda (_: T).(csubst0 (minus (s (Bind b) x2) (s k0 (S n0))) v e1
+e2))))))) (ex4_5_intro K C C T T (\lambda (k0: K).(\lambda (e1: C).(\lambda
+(_: C).(\lambda (u: T).(\lambda (_: T).(eq C (CHead x4 x3 x6) (CHead e1 k0
+u))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (_:
+T).(\lambda (w: T).(drop (S n0) O (CHead x1 (Bind b) x0) (CHead e2 k0
+w))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (_: C).(\lambda (u:
+T).(\lambda (w: T).(subst0 (minus (s (Bind b) x2) (s k0 (S n0))) v u w))))))
+(\lambda (k0: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
+(_: T).(csubst0 (minus (s (Bind b) x2) (s k0 (S n0))) v e1 e2)))))) x3 x4 x5
+x6 x7 (refl_equal C (CHead x4 x3 x6)) (drop_drop (Bind b) n0 x1 (CHead x5 x3
+x7) H16 x0) (eq_ind_r nat (S (s x3 n0)) (\lambda (n1: nat).(subst0 (minus (s
+(Bind b) x2) n1) v x6 x7)) H17 (s x3 (S n0)) (s_S x3 n0)) (eq_ind_r nat (S (s
+x3 n0)) (\lambda (n1: nat).(csubst0 (minus (s (Bind b) x2) n1) v x4 x5)) H18
+(s x3 (S n0)) (s_S x3 n0)))) e H15)))))))))) H14)) H13)))))) (\lambda (f:
+F).(\lambda (H10: (drop (r (Flat f) n0) O c e)).(\lambda (H11: ((\forall (c3:
+C).(\forall (v0: T).((csubst0 (s (Flat f) x2) v0 c c3) \to (\forall (e0:
+C).((drop (S n0) O c e0) \to (or4 (drop (S n0) O c3 e0) (ex3_4 K C T T
+(\lambda (k0: K).(\lambda (e1: C).(\lambda (u: T).(\lambda (_: T).(eq C e0
+(CHead e1 k0 u)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda (_:
+T).(\lambda (w: T).(drop (S n0) O c3 (CHead e1 k0 w)))))) (\lambda (k0:
+K).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus (s (Flat f)
+x2) (s k0 (S n0))) v0 u w)))))) (ex3_4 K C C T (\lambda (k0: K).(\lambda (e1:
+C).(\lambda (_: C).(\lambda (u: T).(eq C e0 (CHead e1 k0 u)))))) (\lambda
+(k0: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(drop (S n0) O c3
+(CHead e2 k0 u)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda (e2:
+C).(\lambda (_: T).(csubst0 (minus (s (Flat f) x2) (s k0 (S n0))) v0 e1
+e2)))))) (ex4_5 K C C T T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (_: T).(eq C e0 (CHead e1 k0 u))))))) (\lambda
+(k0: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w:
+T).(drop (S n0) O c3 (CHead e2 k0 w))))))) (\lambda (k0: K).(\lambda (_:
+C).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus (s (Flat f)
+x2) (s k0 (S n0))) v0 u w)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda
+(e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus (s (Flat f) x2) (s k0
+(S n0))) v0 e1 e2))))))))))))))).(\lambda (_: (lt (S n0) (s (Flat f)
+x2))).(let H13 \def (H11 x1 v H7 e H10) in (or4_ind (drop (S n0) O x1 e)
+(ex3_4 K C T T (\lambda (k0: K).(\lambda (e0: C).(\lambda (u: T).(\lambda (_:
+T).(eq C e (CHead e0 k0 u)))))) (\lambda (k0: K).(\lambda (e0: C).(\lambda
+(_: T).(\lambda (w: T).(drop (S n0) O x1 (CHead e0 k0 w)))))) (\lambda (k0:
+K).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus x2 (s k0 (S
+n0))) v u w)))))) (ex3_4 K C C T (\lambda (k0: K).(\lambda (e1: C).(\lambda
+(_: C).(\lambda (u: T).(eq C e (CHead e1 k0 u)))))) (\lambda (k0: K).(\lambda
+(_: C).(\lambda (e2: C).(\lambda (u: T).(drop (S n0) O x1 (CHead e2 k0
+u)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
+T).(csubst0 (minus x2 (s k0 (S n0))) v e1 e2)))))) (ex4_5 K C C T T (\lambda
+(k0: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq
+C e (CHead e1 k0 u))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O x1 (CHead e2 k0 w)))))))
+(\lambda (k0: K).(\lambda (_: C).(\lambda (_: C).(\lambda (u: T).(\lambda (w:
+T).(subst0 (minus x2 (s k0 (S n0))) v u w)))))) (\lambda (k0: K).(\lambda
+(e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus x2
+(s k0 (S n0))) v e1 e2))))))) (or4 (drop (S n0) O (CHead x1 (Flat f) x0) e)
+(ex3_4 K C T T (\lambda (k0: K).(\lambda (e0: C).(\lambda (u: T).(\lambda (_:
+T).(eq C e (CHead e0 k0 u)))))) (\lambda (k0: K).(\lambda (e0: C).(\lambda
+(_: T).(\lambda (w: T).(drop (S n0) O (CHead x1 (Flat f) x0) (CHead e0 k0
+w)))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (u: T).(\lambda (w:
+T).(subst0 (minus (s (Flat f) x2) (s k0 (S n0))) v u w)))))) (ex3_4 K C C T
+(\lambda (k0: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(eq C e
+(CHead e1 k0 u)))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (u: T).(drop (S n0) O (CHead x1 (Flat f) x0) (CHead e2 k0 u))))))
+(\lambda (k0: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0
+(minus (s (Flat f) x2) (s k0 (S n0))) v e1 e2)))))) (ex4_5 K C C T T (\lambda
+(k0: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq
+C e (CHead e1 k0 u))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead x1 (Flat f) x0)
+(CHead e2 k0 w))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus (s (Flat f) x2) (s k0 (S
+n0))) v u w)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda
+(_: T).(\lambda (_: T).(csubst0 (minus (s (Flat f) x2) (s k0 (S n0))) v e1
+e2)))))))) (\lambda (H14: (drop (S n0) O x1 e)).(or4_intro0 (drop (S n0) O
+(CHead x1 (Flat f) x0) e) (ex3_4 K C T T (\lambda (k0: K).(\lambda (e0:
+C).(\lambda (u: T).(\lambda (_: T).(eq C e (CHead e0 k0 u)))))) (\lambda (k0:
+K).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead x1
+(Flat f) x0) (CHead e0 k0 w)))))) (\lambda (k0: K).(\lambda (_: C).(\lambda
+(u: T).(\lambda (w: T).(subst0 (minus (s (Flat f) x2) (s k0 (S n0))) v u
+w)))))) (ex3_4 K C C T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u: T).(eq C e (CHead e1 k0 u)))))) (\lambda (k0: K).(\lambda (_:
+C).(\lambda (e2: C).(\lambda (u: T).(drop (S n0) O (CHead x1 (Flat f) x0)
+(CHead e2 k0 u)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda (e2:
+C).(\lambda (_: T).(csubst0 (minus (s (Flat f) x2) (s k0 (S n0))) v e1
+e2)))))) (ex4_5 K C C T T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (_: T).(eq C e (CHead e1 k0 u))))))) (\lambda
+(k0: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w:
+T).(drop (S n0) O (CHead x1 (Flat f) x0) (CHead e2 k0 w))))))) (\lambda (k0:
+K).(\lambda (_: C).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0
+(minus (s (Flat f) x2) (s k0 (S n0))) v u w)))))) (\lambda (k0: K).(\lambda
+(e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus (s
+(Flat f) x2) (s k0 (S n0))) v e1 e2))))))) (drop_drop (Flat f) n0 x1 e H14
+x0))) (\lambda (H14: (ex3_4 K C T T (\lambda (k0: K).(\lambda (e0:
+C).(\lambda (u: T).(\lambda (_: T).(eq C e (CHead e0 k0 u)))))) (\lambda (k0:
+K).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O x1 (CHead
+e0 k0 w)))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (u: T).(\lambda (w:
+T).(subst0 (minus x2 (s k0 (S n0))) v u w))))))).(ex3_4_ind K C T T (\lambda
+(k0: K).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C e (CHead e0 k0
+u)))))) (\lambda (k0: K).(\lambda (e0: C).(\lambda (_: T).(\lambda (w:
+T).(drop (S n0) O x1 (CHead e0 k0 w)))))) (\lambda (k0: K).(\lambda (_:
+C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus x2 (s k0 (S n0))) v u
+w))))) (or4 (drop (S n0) O (CHead x1 (Flat f) x0) e) (ex3_4 K C T T (\lambda
+(k0: K).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C e (CHead e0 k0
+u)))))) (\lambda (k0: K).(\lambda (e0: C).(\lambda (_: T).(\lambda (w:
+T).(drop (S n0) O (CHead x1 (Flat f) x0) (CHead e0 k0 w)))))) (\lambda (k0:
+K).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus (s (Flat f)
+x2) (s k0 (S n0))) v u w)))))) (ex3_4 K C C T (\lambda (k0: K).(\lambda (e1:
+C).(\lambda (_: C).(\lambda (u: T).(eq C e (CHead e1 k0 u)))))) (\lambda (k0:
+K).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(drop (S n0) O (CHead x1
+(Flat f) x0) (CHead e2 k0 u)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda
+(e2: C).(\lambda (_: T).(csubst0 (minus (s (Flat f) x2) (s k0 (S n0))) v e1
+e2)))))) (ex4_5 K C C T T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (_: T).(eq C e (CHead e1 k0 u))))))) (\lambda
+(k0: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w:
+T).(drop (S n0) O (CHead x1 (Flat f) x0) (CHead e2 k0 w))))))) (\lambda (k0:
+K).(\lambda (_: C).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0
+(minus (s (Flat f) x2) (s k0 (S n0))) v u w)))))) (\lambda (k0: K).(\lambda
+(e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus (s
+(Flat f) x2) (s k0 (S n0))) v e1 e2)))))))) (\lambda (x3: K).(\lambda (x4:
+C).(\lambda (x5: T).(\lambda (x6: T).(\lambda (H15: (eq C e (CHead x4 x3
+x5))).(\lambda (H16: (drop (S n0) O x1 (CHead x4 x3 x6))).(\lambda (H17:
+(subst0 (minus x2 (s x3 (S n0))) v x5 x6)).(eq_ind_r C (CHead x4 x3 x5)
+(\lambda (c0: C).(or4 (drop (S n0) O (CHead x1 (Flat f) x0) c0) (ex3_4 K C T
+T (\lambda (k0: K).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C c0
+(CHead e0 k0 u)))))) (\lambda (k0: K).(\lambda (e0: C).(\lambda (_:
+T).(\lambda (w: T).(drop (S n0) O (CHead x1 (Flat f) x0) (CHead e0 k0 w))))))
+(\lambda (k0: K).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0
+(minus (s (Flat f) x2) (s k0 (S n0))) v u w)))))) (ex3_4 K C C T (\lambda
+(k0: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(eq C c0 (CHead e1
+k0 u)))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (u:
+T).(drop (S n0) O (CHead x1 (Flat f) x0) (CHead e2 k0 u)))))) (\lambda (k0:
+K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (minus (s (Flat
+f) x2) (s k0 (S n0))) v e1 e2)))))) (ex4_5 K C C T T (\lambda (k0:
+K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq C c0
+(CHead e1 k0 u))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead x1 (Flat f) x0)
+(CHead e2 k0 w))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus (s (Flat f) x2) (s k0 (S
+n0))) v u w)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda
+(_: T).(\lambda (_: T).(csubst0 (minus (s (Flat f) x2) (s k0 (S n0))) v e1
+e2))))))))) (or4_intro1 (drop (S n0) O (CHead x1 (Flat f) x0) (CHead x4 x3
+x5)) (ex3_4 K C T T (\lambda (k0: K).(\lambda (e0: C).(\lambda (u:
+T).(\lambda (_: T).(eq C (CHead x4 x3 x5) (CHead e0 k0 u)))))) (\lambda (k0:
+K).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead x1
+(Flat f) x0) (CHead e0 k0 w)))))) (\lambda (k0: K).(\lambda (_: C).(\lambda
+(u: T).(\lambda (w: T).(subst0 (minus (s (Flat f) x2) (s k0 (S n0))) v u
+w)))))) (ex3_4 K C C T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u: T).(eq C (CHead x4 x3 x5) (CHead e1 k0 u)))))) (\lambda (k0:
+K).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(drop (S n0) O (CHead x1
+(Flat f) x0) (CHead e2 k0 u)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda
+(e2: C).(\lambda (_: T).(csubst0 (minus (s (Flat f) x2) (s k0 (S n0))) v e1
+e2)))))) (ex4_5 K C C T T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (_: T).(eq C (CHead x4 x3 x5) (CHead e1 k0
+u))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (_:
+T).(\lambda (w: T).(drop (S n0) O (CHead x1 (Flat f) x0) (CHead e2 k0
+w))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (_: C).(\lambda (u:
+T).(\lambda (w: T).(subst0 (minus (s (Flat f) x2) (s k0 (S n0))) v u w))))))
+(\lambda (k0: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
+(_: T).(csubst0 (minus (s (Flat f) x2) (s k0 (S n0))) v e1 e2)))))))
+(ex3_4_intro K C T T (\lambda (k0: K).(\lambda (e0: C).(\lambda (u:
+T).(\lambda (_: T).(eq C (CHead x4 x3 x5) (CHead e0 k0 u)))))) (\lambda (k0:
+K).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead x1
+(Flat f) x0) (CHead e0 k0 w)))))) (\lambda (k0: K).(\lambda (_: C).(\lambda
+(u: T).(\lambda (w: T).(subst0 (minus (s (Flat f) x2) (s k0 (S n0))) v u
+w))))) x3 x4 x5 x6 (refl_equal C (CHead x4 x3 x5)) (drop_drop (Flat f) n0 x1
+(CHead x4 x3 x6) H16 x0) H17)) e H15)))))))) H14)) (\lambda (H14: (ex3_4 K C
+C T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(eq C e
+(CHead e1 k0 u)))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (u: T).(drop (S n0) O x1 (CHead e2 k0 u)))))) (\lambda (k0:
+K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (minus x2 (s k0
+(S n0))) v e1 e2))))))).(ex3_4_ind K C C T (\lambda (k0: K).(\lambda (e1:
+C).(\lambda (_: C).(\lambda (u: T).(eq C e (CHead e1 k0 u)))))) (\lambda (k0:
+K).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(drop (S n0) O x1 (CHead
+e2 k0 u)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
+T).(csubst0 (minus x2 (s k0 (S n0))) v e1 e2))))) (or4 (drop (S n0) O (CHead
+x1 (Flat f) x0) e) (ex3_4 K C T T (\lambda (k0: K).(\lambda (e0: C).(\lambda
+(u: T).(\lambda (_: T).(eq C e (CHead e0 k0 u)))))) (\lambda (k0: K).(\lambda
+(e0: C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead x1 (Flat f) x0)
+(CHead e0 k0 w)))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (u:
+T).(\lambda (w: T).(subst0 (minus (s (Flat f) x2) (s k0 (S n0))) v u w))))))
+(ex3_4 K C C T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u:
+T).(eq C e (CHead e1 k0 u)))))) (\lambda (k0: K).(\lambda (_: C).(\lambda
+(e2: C).(\lambda (u: T).(drop (S n0) O (CHead x1 (Flat f) x0) (CHead e2 k0
+u)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
+T).(csubst0 (minus (s (Flat f) x2) (s k0 (S n0))) v e1 e2)))))) (ex4_5 K C C
+T T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u:
+T).(\lambda (_: T).(eq C e (CHead e1 k0 u))))))) (\lambda (k0: K).(\lambda
+(_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead
+x1 (Flat f) x0) (CHead e2 k0 w))))))) (\lambda (k0: K).(\lambda (_:
+C).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus (s (Flat f)
+x2) (s k0 (S n0))) v u w)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda
+(e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus (s (Flat f) x2) (s k0
+(S n0))) v e1 e2)))))))) (\lambda (x3: K).(\lambda (x4: C).(\lambda (x5:
+C).(\lambda (x6: T).(\lambda (H15: (eq C e (CHead x4 x3 x6))).(\lambda (H16:
+(drop (S n0) O x1 (CHead x5 x3 x6))).(\lambda (H17: (csubst0 (minus x2 (s x3
+(S n0))) v x4 x5)).(eq_ind_r C (CHead x4 x3 x6) (\lambda (c0: C).(or4 (drop
+(S n0) O (CHead x1 (Flat f) x0) c0) (ex3_4 K C T T (\lambda (k0: K).(\lambda
+(e0: C).(\lambda (u: T).(\lambda (_: T).(eq C c0 (CHead e0 k0 u))))))
+(\lambda (k0: K).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(drop (S
+n0) O (CHead x1 (Flat f) x0) (CHead e0 k0 w)))))) (\lambda (k0: K).(\lambda
+(_: C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus (s (Flat f) x2) (s k0
+(S n0))) v u w)))))) (ex3_4 K C C T (\lambda (k0: K).(\lambda (e1:
+C).(\lambda (_: C).(\lambda (u: T).(eq C c0 (CHead e1 k0 u)))))) (\lambda
+(k0: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(drop (S n0) O
+(CHead x1 (Flat f) x0) (CHead e2 k0 u)))))) (\lambda (k0: K).(\lambda (e1:
+C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (minus (s (Flat f) x2) (s k0 (S
+n0))) v e1 e2)))))) (ex4_5 K C C T T (\lambda (k0: K).(\lambda (e1:
+C).(\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq C c0 (CHead e1 k0
+u))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (_:
+T).(\lambda (w: T).(drop (S n0) O (CHead x1 (Flat f) x0) (CHead e2 k0
+w))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (_: C).(\lambda (u:
+T).(\lambda (w: T).(subst0 (minus (s (Flat f) x2) (s k0 (S n0))) v u w))))))
+(\lambda (k0: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
+(_: T).(csubst0 (minus (s (Flat f) x2) (s k0 (S n0))) v e1 e2)))))))))
+(or4_intro2 (drop (S n0) O (CHead x1 (Flat f) x0) (CHead x4 x3 x6)) (ex3_4 K
+C T T (\lambda (k0: K).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C
+(CHead x4 x3 x6) (CHead e0 k0 u)))))) (\lambda (k0: K).(\lambda (e0:
+C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead x1 (Flat f) x0)
+(CHead e0 k0 w)))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (u:
+T).(\lambda (w: T).(subst0 (minus (s (Flat f) x2) (s k0 (S n0))) v u w))))))
+(ex3_4 K C C T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u:
+T).(eq C (CHead x4 x3 x6) (CHead e1 k0 u)))))) (\lambda (k0: K).(\lambda (_:
+C).(\lambda (e2: C).(\lambda (u: T).(drop (S n0) O (CHead x1 (Flat f) x0)
+(CHead e2 k0 u)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda (e2:
+C).(\lambda (_: T).(csubst0 (minus (s (Flat f) x2) (s k0 (S n0))) v e1
+e2)))))) (ex4_5 K C C T T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (_: T).(eq C (CHead x4 x3 x6) (CHead e1 k0
+u))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (_:
+T).(\lambda (w: T).(drop (S n0) O (CHead x1 (Flat f) x0) (CHead e2 k0
+w))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (_: C).(\lambda (u:
+T).(\lambda (w: T).(subst0 (minus (s (Flat f) x2) (s k0 (S n0))) v u w))))))
+(\lambda (k0: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
+(_: T).(csubst0 (minus (s (Flat f) x2) (s k0 (S n0))) v e1 e2)))))))
+(ex3_4_intro K C C T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u: T).(eq C (CHead x4 x3 x6) (CHead e1 k0 u)))))) (\lambda (k0:
+K).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(drop (S n0) O (CHead x1
+(Flat f) x0) (CHead e2 k0 u)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda
+(e2: C).(\lambda (_: T).(csubst0 (minus (s (Flat f) x2) (s k0 (S n0))) v e1
+e2))))) x3 x4 x5 x6 (refl_equal C (CHead x4 x3 x6)) (drop_drop (Flat f) n0 x1
+(CHead x5 x3 x6) H16 x0) H17)) e H15)))))))) H14)) (\lambda (H14: (ex4_5 K C
+C T T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u:
+T).(\lambda (_: T).(eq C e (CHead e1 k0 u))))))) (\lambda (k0: K).(\lambda
+(_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O x1
+(CHead e2 k0 w))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus x2 (s k0 (S n0))) v u
+w)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
+T).(\lambda (_: T).(csubst0 (minus x2 (s k0 (S n0))) v e1
+e2)))))))).(ex4_5_ind K C C T T (\lambda (k0: K).(\lambda (e1: C).(\lambda
+(_: C).(\lambda (u: T).(\lambda (_: T).(eq C e (CHead e1 k0 u))))))) (\lambda
+(k0: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w:
+T).(drop (S n0) O x1 (CHead e2 k0 w))))))) (\lambda (k0: K).(\lambda (_:
+C).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus x2 (s k0 (S
+n0))) v u w)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda
+(_: T).(\lambda (_: T).(csubst0 (minus x2 (s k0 (S n0))) v e1 e2)))))) (or4
+(drop (S n0) O (CHead x1 (Flat f) x0) e) (ex3_4 K C T T (\lambda (k0:
+K).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C e (CHead e0 k0
+u)))))) (\lambda (k0: K).(\lambda (e0: C).(\lambda (_: T).(\lambda (w:
+T).(drop (S n0) O (CHead x1 (Flat f) x0) (CHead e0 k0 w)))))) (\lambda (k0:
+K).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus (s (Flat f)
+x2) (s k0 (S n0))) v u w)))))) (ex3_4 K C C T (\lambda (k0: K).(\lambda (e1:
+C).(\lambda (_: C).(\lambda (u: T).(eq C e (CHead e1 k0 u)))))) (\lambda (k0:
+K).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(drop (S n0) O (CHead x1
+(Flat f) x0) (CHead e2 k0 u)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda
+(e2: C).(\lambda (_: T).(csubst0 (minus (s (Flat f) x2) (s k0 (S n0))) v e1
+e2)))))) (ex4_5 K C C T T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (_: T).(eq C e (CHead e1 k0 u))))))) (\lambda
+(k0: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w:
+T).(drop (S n0) O (CHead x1 (Flat f) x0) (CHead e2 k0 w))))))) (\lambda (k0:
+K).(\lambda (_: C).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0
+(minus (s (Flat f) x2) (s k0 (S n0))) v u w)))))) (\lambda (k0: K).(\lambda
+(e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 (minus (s
+(Flat f) x2) (s k0 (S n0))) v e1 e2)))))))) (\lambda (x3: K).(\lambda (x4:
+C).(\lambda (x5: C).(\lambda (x6: T).(\lambda (x7: T).(\lambda (H15: (eq C e
+(CHead x4 x3 x6))).(\lambda (H16: (drop (S n0) O x1 (CHead x5 x3
+x7))).(\lambda (H17: (subst0 (minus x2 (s x3 (S n0))) v x6 x7)).(\lambda
+(H18: (csubst0 (minus x2 (s x3 (S n0))) v x4 x5)).(eq_ind_r C (CHead x4 x3
+x6) (\lambda (c0: C).(or4 (drop (S n0) O (CHead x1 (Flat f) x0) c0) (ex3_4 K
+C T T (\lambda (k0: K).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C
+c0 (CHead e0 k0 u)))))) (\lambda (k0: K).(\lambda (e0: C).(\lambda (_:
+T).(\lambda (w: T).(drop (S n0) O (CHead x1 (Flat f) x0) (CHead e0 k0 w))))))
+(\lambda (k0: K).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0
+(minus (s (Flat f) x2) (s k0 (S n0))) v u w)))))) (ex3_4 K C C T (\lambda
+(k0: K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(eq C c0 (CHead e1
+k0 u)))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (u:
+T).(drop (S n0) O (CHead x1 (Flat f) x0) (CHead e2 k0 u)))))) (\lambda (k0:
+K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (minus (s (Flat
+f) x2) (s k0 (S n0))) v e1 e2)))))) (ex4_5 K C C T T (\lambda (k0:
+K).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq C c0
+(CHead e1 k0 u))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead x1 (Flat f) x0)
+(CHead e2 k0 w))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (w: T).(subst0 (minus (s (Flat f) x2) (s k0 (S
+n0))) v u w)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda
+(_: T).(\lambda (_: T).(csubst0 (minus (s (Flat f) x2) (s k0 (S n0))) v e1
+e2))))))))) (or4_intro3 (drop (S n0) O (CHead x1 (Flat f) x0) (CHead x4 x3
+x6)) (ex3_4 K C T T (\lambda (k0: K).(\lambda (e0: C).(\lambda (u:
+T).(\lambda (_: T).(eq C (CHead x4 x3 x6) (CHead e0 k0 u)))))) (\lambda (k0:
+K).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(drop (S n0) O (CHead x1
+(Flat f) x0) (CHead e0 k0 w)))))) (\lambda (k0: K).(\lambda (_: C).(\lambda
+(u: T).(\lambda (w: T).(subst0 (minus (s (Flat f) x2) (s k0 (S n0))) v u
+w)))))) (ex3_4 K C C T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u: T).(eq C (CHead x4 x3 x6) (CHead e1 k0 u)))))) (\lambda (k0:
+K).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(drop (S n0) O (CHead x1
+(Flat f) x0) (CHead e2 k0 u)))))) (\lambda (k0: K).(\lambda (e1: C).(\lambda
+(e2: C).(\lambda (_: T).(csubst0 (minus (s (Flat f) x2) (s k0 (S n0))) v e1
+e2)))))) (ex4_5 K C C T T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (_: T).(eq C (CHead x4 x3 x6) (CHead e1 k0
+u))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (_:
+T).(\lambda (w: T).(drop (S n0) O (CHead x1 (Flat f) x0) (CHead e2 k0
+w))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (_: C).(\lambda (u:
+T).(\lambda (w: T).(subst0 (minus (s (Flat f) x2) (s k0 (S n0))) v u w))))))
+(\lambda (k0: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
+(_: T).(csubst0 (minus (s (Flat f) x2) (s k0 (S n0))) v e1 e2)))))))
+(ex4_5_intro K C C T T (\lambda (k0: K).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (_: T).(eq C (CHead x4 x3 x6) (CHead e1 k0
+u))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (e2: C).(\lambda (_:
+T).(\lambda (w: T).(drop (S n0) O (CHead x1 (Flat f) x0) (CHead e2 k0
+w))))))) (\lambda (k0: K).(\lambda (_: C).(\lambda (_: C).(\lambda (u:
+T).(\lambda (w: T).(subst0 (minus (s (Flat f) x2) (s k0 (S n0))) v u w))))))
+(\lambda (k0: K).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
+(_: T).(csubst0 (minus (s (Flat f) x2) (s k0 (S n0))) v e1 e2)))))) x3 x4 x5
+x6 x7 (refl_equal C (CHead x4 x3 x6)) (drop_drop (Flat f) n0 x1 (CHead x5 x3
+x7) H16 x0) H17 H18)) e H15)))))))))) H14)) H13)))))) k (drop_gen_drop k c e
+t n0 H2) H8 H9) i H4))) c2 H5)))))))) H3)) (csubst0_gen_head k c c2 t v i
+H1))))))))))) c1)))))) n).
+
+theorem csubst0_drop_eq:
+ \forall (n: nat).(\forall (c1: C).(\forall (c2: C).(\forall (v: T).((csubst0
+n v c1 c2) \to (\forall (e: C).((drop n O c1 e) \to (or4 (drop n O c2 e)
+(ex3_4 F C T T (\lambda (f: F).(\lambda (e0: C).(\lambda (u: T).(\lambda (_:
+T).(eq C e (CHead e0 (Flat f) u)))))) (\lambda (f: F).(\lambda (e0:
+C).(\lambda (_: T).(\lambda (w: T).(drop n O c2 (CHead e0 (Flat f) w))))))
+(\lambda (_: F).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 O v u
+w)))))) (ex3_4 F C C T (\lambda (f: F).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u: T).(eq C e (CHead e1 (Flat f) u)))))) (\lambda (f:
+F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(drop n O c2 (CHead e2
+(Flat f) u)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda
+(_: T).(csubst0 O v e1 e2)))))) (ex4_5 F C C T T (\lambda (f: F).(\lambda
+(e1: C).(\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq C e (CHead e1
+(Flat f) u))))))) (\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda
+(_: T).(\lambda (w: T).(drop n O c2 (CHead e2 (Flat f) w))))))) (\lambda (_:
+F).(\lambda (_: C).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 O
+v u w)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
+T).(\lambda (_: T).(csubst0 O v e1 e2))))))))))))))