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))))))))) (insert_eq nat O (\lambda (n0: nat).(csubst0 n0 v c1 c2))
-(or4 (drop O O c2 c1) (ex3_4 F C T T (\lambda (f: F).(\lambda (e0:
-C).(\lambda (u: T).(\lambda (_: T).(eq C c1 (CHead e0 (Flat f) u))))))
-(\lambda (f: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(drop O 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 c1 (CHead e1 (Flat
-f) u)))))) (\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u:
-T).(drop O 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 c1 (CHead e1 (Flat f) u))))))) (\lambda (f: F).(\lambda (_:
-C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(drop O 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)))))))) (\lambda (y: nat).(\lambda (H1: (csubst0 y v c1 c2)).(csubst0_ind
-(\lambda (n0: nat).(\lambda (t: T).(\lambda (c: C).(\lambda (c0: C).((eq nat
-n0 O) \to (or4 (drop O O c0 c) (ex3_4 F C T T (\lambda (f: F).(\lambda (e0:
-C).(\lambda (u: T).(\lambda (_: T).(eq C c (CHead e0 (Flat f) u))))))
-(\lambda (f: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(drop O O c0
-(CHead e0 (Flat f) w)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u:
-T).(\lambda (w: T).(subst0 O t u w)))))) (ex3_4 F C C T (\lambda (f:
-F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(eq C c (CHead e1 (Flat
-f) u)))))) (\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u:
-T).(drop O O c0 (CHead e2 (Flat f) u)))))) (\lambda (_: F).(\lambda (e1:
-C).(\lambda (e2: C).(\lambda (_: T).(csubst0 O t e1 e2)))))) (ex4_5 F C C T T
-(\lambda (f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(\lambda (_:
-T).(eq C c (CHead e1 (Flat f) u))))))) (\lambda (f: F).(\lambda (_:
-C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(drop O O c0 (CHead e2
-(Flat f) w))))))) (\lambda (_: F).(\lambda (_: C).(\lambda (_: C).(\lambda
-(u: T).(\lambda (w: T).(subst0 O t u w)))))) (\lambda (_: F).(\lambda (e1:
-C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 O t e1
-e2))))))))))))) (\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i:
-nat).(\forall (v0: T).(\forall (u1: T).(\forall (u2: T).((subst0 i v0 u1 u2)
-\to (\forall (c: C).((eq nat (s k0 i) O) \to (or4 (drop O O (CHead c k0 u2)
-(CHead c k0 u1)) (ex3_4 F C T T (\lambda (f: F).(\lambda (e0: C).(\lambda (u:
-T).(\lambda (_: T).(eq C (CHead c k0 u1) (CHead e0 (Flat f) u)))))) (\lambda
-(f: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(drop O O (CHead c k0
-u2) (CHead e0 (Flat f) w)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u:
-T).(\lambda (w: T).(subst0 O v0 u w)))))) (ex3_4 F C C T (\lambda (f:
-F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(eq C (CHead c k0 u1)
+(\lambda (n0: nat).(or4 (drop n0 n0 c2 c1) (ex3_4 F C T T (\lambda (f:
+F).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C c1 (CHead e0 (Flat
+f) u)))))) (\lambda (f: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (w:
+T).(drop n0 n0 c2 (CHead e0 (Flat f) w)))))) (\lambda (_: F).(\lambda (_:
+C).(\lambda (u: T).(\lambda (w: T).(subst0 n0 v u w)))))) (ex3_4 F C C T
+(\lambda (f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(eq C c1
(CHead e1 (Flat f) u)))))) (\lambda (f: F).(\lambda (_: C).(\lambda (e2:
-C).(\lambda (u: T).(drop O O (CHead c k0 u2) (CHead e2 (Flat f) u))))))
-(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 O
-v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f: F).(\lambda (e1: C).(\lambda (_:
-C).(\lambda (u: T).(\lambda (_: T).(eq C (CHead c k0 u1) (CHead e1 (Flat f)
-u))))))) (\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (_:
-T).(\lambda (w: T).(drop O O (CHead c k0 u2) (CHead e2 (Flat f) w)))))))
-(\lambda (_: F).(\lambda (_: C).(\lambda (_: C).(\lambda (u: T).(\lambda (w:
-T).(subst0 O v0 u w)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2:
-C).(\lambda (_: T).(\lambda (_: T).(csubst0 O v0 e1 e2))))))))))))))))
-(\lambda (b: B).(\lambda (i: nat).(\lambda (v0: T).(\lambda (u1: T).(\lambda
-(u2: T).(\lambda (_: (subst0 i v0 u1 u2)).(\lambda (c: C).(\lambda (H3: (eq
-nat (S i) O)).(let H4 \def (eq_ind nat (S i) (\lambda (ee: nat).(match ee in
-nat return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _)
-\Rightarrow True])) I O H3) in (False_ind (or4 (drop O O (CHead c (Bind b)
-u2) (CHead c (Bind b) u1)) (ex3_4 F C T T (\lambda (f: F).(\lambda (e0:
-C).(\lambda (u: T).(\lambda (_: T).(eq C (CHead c (Bind b) u1) (CHead e0
-(Flat f) u)))))) (\lambda (f: F).(\lambda (e0: C).(\lambda (_: T).(\lambda
-(w: T).(drop O O (CHead c (Bind b) u2) (CHead e0 (Flat f) w)))))) (\lambda
-(_: F).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 O v0 u w))))))
+C).(\lambda (u: T).(drop n0 n0 c2 (CHead e2 (Flat f) u)))))) (\lambda (_:
+F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 n0 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 c1 (CHead e1 (Flat f) u)))))))
+(\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w:
+T).(drop n0 n0 c2 (CHead e2 (Flat f) w))))))) (\lambda (_: F).(\lambda (_:
+C).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 n0 v u w))))))
+(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
+(_: T).(csubst0 n0 v e1 e2))))))))) (\lambda (y: nat).(\lambda (H1: (csubst0
+y v c1 c2)).(csubst0_ind (\lambda (n0: nat).(\lambda (t: T).(\lambda (c:
+C).(\lambda (c0: C).((eq nat n0 O) \to (or4 (drop n0 n0 c0 c) (ex3_4 F C T T
+(\lambda (f: F).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C c
+(CHead e0 (Flat f) u)))))) (\lambda (f: F).(\lambda (e0: C).(\lambda (_:
+T).(\lambda (w: T).(drop n0 n0 c0 (CHead e0 (Flat f) w)))))) (\lambda (_:
+F).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 n0 t u w))))))
(ex3_4 F C C T (\lambda (f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u:
-T).(eq C (CHead c (Bind b) u1) (CHead e1 (Flat f) u)))))) (\lambda (f:
-F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(drop O O (CHead c (Bind
-b) u2) (CHead e2 (Flat f) u)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda
-(e2: C).(\lambda (_: T).(csubst0 O v0 e1 e2)))))) (ex4_5 F C C T T (\lambda
-(f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq C
-(CHead c (Bind b) u1) (CHead e1 (Flat f) u))))))) (\lambda (f: F).(\lambda
-(_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(drop O O (CHead c
-(Bind b) u2) (CHead e2 (Flat f) w))))))) (\lambda (_: F).(\lambda (_:
-C).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 O v0 u w))))))
+T).(eq C c (CHead e1 (Flat f) u)))))) (\lambda (f: F).(\lambda (_:
+C).(\lambda (e2: C).(\lambda (u: T).(drop n0 n0 c0 (CHead e2 (Flat f) u))))))
+(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 n0
+t e1 e2)))))) (ex4_5 F C C T T (\lambda (f: F).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (_: T).(eq C c (CHead e1 (Flat f) u)))))))
+(\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w:
+T).(drop n0 n0 c0 (CHead e2 (Flat f) w))))))) (\lambda (_: F).(\lambda (_:
+C).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 n0 t u w))))))
(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
-(_: T).(csubst0 O v0 e1 e2)))))))) H4)))))))))) (\lambda (f: F).(\lambda (i:
+(_: T).(csubst0 n0 t e1 e2))))))))))))) (\lambda (k: K).(K_ind (\lambda (k0:
+K).(\forall (i: nat).(\forall (v0: T).(\forall (u1: T).(\forall (u2:
+T).((subst0 i v0 u1 u2) \to (\forall (c: C).((eq nat (s k0 i) O) \to (or4
+(drop (s k0 i) (s k0 i) (CHead c k0 u2) (CHead c k0 u1)) (ex3_4 F C T T
+(\lambda (f: F).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C (CHead
+c k0 u1) (CHead e0 (Flat f) u)))))) (\lambda (f: F).(\lambda (e0: C).(\lambda
+(_: T).(\lambda (w: T).(drop (s k0 i) (s k0 i) (CHead c k0 u2) (CHead e0
+(Flat f) w)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u: T).(\lambda (w:
+T).(subst0 (s k0 i) v0 u w)))))) (ex3_4 F C C T (\lambda (f: F).(\lambda (e1:
+C).(\lambda (_: C).(\lambda (u: T).(eq C (CHead c k0 u1) (CHead e1 (Flat f)
+u)))))) (\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u:
+T).(drop (s k0 i) (s k0 i) (CHead c k0 u2) (CHead e2 (Flat f) u))))))
+(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (s
+k0 i) v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f: F).(\lambda (e1:
+C).(\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq C (CHead c k0 u1)
+(CHead e1 (Flat f) u))))))) (\lambda (f: F).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (_: T).(\lambda (w: T).(drop (s k0 i) (s k0 i) (CHead c k0 u2)
+(CHead e2 (Flat f) w))))))) (\lambda (_: F).(\lambda (_: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (w: T).(subst0 (s k0 i) v0 u w)))))) (\lambda (_:
+F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0
+(s k0 i) v0 e1 e2)))))))))))))))) (\lambda (b: B).(\lambda (i: nat).(\lambda
+(v0: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (subst0 i v0 u1
+u2)).(\lambda (c: C).(\lambda (H3: (eq nat (S i) O)).(let H4 \def (eq_ind nat
+(S i) (\lambda (ee: nat).(match ee in nat return (\lambda (_: nat).Prop) with
+[O \Rightarrow False | (S _) \Rightarrow True])) I O H3) in (False_ind (or4
+(drop (S i) (S i) (CHead c (Bind b) u2) (CHead c (Bind b) u1)) (ex3_4 F C T T
+(\lambda (f: F).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C (CHead
+c (Bind b) u1) (CHead e0 (Flat f) u)))))) (\lambda (f: F).(\lambda (e0:
+C).(\lambda (_: T).(\lambda (w: T).(drop (S i) (S i) (CHead c (Bind b) u2)
+(CHead e0 (Flat f) w)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u:
+T).(\lambda (w: T).(subst0 (S i) v0 u w)))))) (ex3_4 F C C T (\lambda (f:
+F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(eq C (CHead c (Bind b)
+u1) (CHead e1 (Flat f) u)))))) (\lambda (f: F).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (u: T).(drop (S i) (S i) (CHead c (Bind b) u2) (CHead e2 (Flat f)
+u)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
+T).(csubst0 (S i) v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f: F).(\lambda
+(e1: C).(\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq C (CHead c (Bind
+b) u1) (CHead e1 (Flat f) u))))))) (\lambda (f: F).(\lambda (_: C).(\lambda
+(e2: C).(\lambda (_: T).(\lambda (w: T).(drop (S i) (S i) (CHead c (Bind b)
+u2) (CHead e2 (Flat f) w))))))) (\lambda (_: F).(\lambda (_: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (w: T).(subst0 (S i) v0 u w)))))) (\lambda (_:
+F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0
+(S i) v0 e1 e2)))))))) H4)))))))))) (\lambda (f: F).(\lambda (i:
nat).(\lambda (v0: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (H2: (subst0
i v0 u1 u2)).(\lambda (c: C).(\lambda (H3: (eq nat i O)).(let H4 \def (eq_ind
-nat i (\lambda (n0: nat).(subst0 n0 v0 u1 u2)) H2 O H3) in (or4_intro1 (drop
-O O (CHead c (Flat f) u2) (CHead c (Flat f) u1)) (ex3_4 F C T T (\lambda (f0:
-F).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C (CHead c (Flat f)
-u1) (CHead e0 (Flat f0) u)))))) (\lambda (f0: F).(\lambda (e0: C).(\lambda
-(_: T).(\lambda (w: T).(drop O O (CHead c (Flat f) u2) (CHead e0 (Flat f0)
-w)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u: T).(\lambda (w:
-T).(subst0 O v0 u w)))))) (ex3_4 F C C T (\lambda (f0: F).(\lambda (e1:
-C).(\lambda (_: C).(\lambda (u: T).(eq C (CHead c (Flat f) u1) (CHead e1
-(Flat f0) u)))))) (\lambda (f0: F).(\lambda (_: C).(\lambda (e2: C).(\lambda
-(u: T).(drop O O (CHead c (Flat f) u2) (CHead e2 (Flat f0) u)))))) (\lambda
-(_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 O v0 e1
-e2)))))) (ex4_5 F C C T T (\lambda (f0: F).(\lambda (e1: C).(\lambda (_:
-C).(\lambda (u: T).(\lambda (_: T).(eq C (CHead c (Flat f) u1) (CHead e1
-(Flat f0) u))))))) (\lambda (f0: F).(\lambda (_: C).(\lambda (e2: C).(\lambda
-(_: T).(\lambda (w: T).(drop O O (CHead c (Flat f) u2) (CHead e2 (Flat f0)
-w))))))) (\lambda (_: F).(\lambda (_: C).(\lambda (_: C).(\lambda (u:
-T).(\lambda (w: T).(subst0 O v0 u w)))))) (\lambda (_: F).(\lambda (e1:
-C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 O v0 e1
-e2))))))) (ex3_4_intro F C T T (\lambda (f0: F).(\lambda (e0: C).(\lambda (u:
+nat i (\lambda (n0: nat).(subst0 n0 v0 u1 u2)) H2 O H3) in (eq_ind_r nat O
+(\lambda (n0: nat).(or4 (drop n0 n0 (CHead c (Flat f) u2) (CHead c (Flat f)
+u1)) (ex3_4 F C T T (\lambda (f0: F).(\lambda (e0: C).(\lambda (u:
T).(\lambda (_: T).(eq C (CHead c (Flat f) u1) (CHead e0 (Flat f0) u))))))
-(\lambda (f0: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(drop O O
+(\lambda (f0: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(drop n0 n0
(CHead c (Flat f) u2) (CHead e0 (Flat f0) w)))))) (\lambda (_: F).(\lambda
-(_: C).(\lambda (u: T).(\lambda (w: T).(subst0 O v0 u w))))) f c u1 u2
-(refl_equal C (CHead c (Flat f) u1)) (drop_refl (CHead c (Flat f) u2))
-H4))))))))))) k)) (\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i:
-nat).(\forall (c3: C).(\forall (c4: C).(\forall (v0: T).((csubst0 i v0 c3 c4)
-\to ((((eq nat i O) \to (or4 (drop O O c4 c3) (ex3_4 F C T T (\lambda (f:
-F).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C c3 (CHead e0 (Flat
-f) u)))))) (\lambda (f: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (w:
-T).(drop O O c4 (CHead e0 (Flat f) w)))))) (\lambda (_: F).(\lambda (_:
-C).(\lambda (u: T).(\lambda (w: T).(subst0 O v0 u w)))))) (ex3_4 F C C T
-(\lambda (f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(eq C c3
-(CHead e1 (Flat f) u)))))) (\lambda (f: F).(\lambda (_: C).(\lambda (e2:
-C).(\lambda (u: T).(drop O O c4 (CHead e2 (Flat f) u)))))) (\lambda (_:
-F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 O v0 e1
-e2)))))) (ex4_5 F C C T T (\lambda (f: F).(\lambda (e1: C).(\lambda (_:
-C).(\lambda (u: T).(\lambda (_: T).(eq C c3 (CHead e1 (Flat f) u)))))))
-(\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w:
-T).(drop O O c4 (CHead e2 (Flat f) w))))))) (\lambda (_: F).(\lambda (_:
-C).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 O v0 u w))))))
+(_: C).(\lambda (u: T).(\lambda (w: T).(subst0 n0 v0 u w)))))) (ex3_4 F C C T
+(\lambda (f0: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(eq C
+(CHead c (Flat f) u1) (CHead e1 (Flat f0) u)))))) (\lambda (f0: F).(\lambda
+(_: C).(\lambda (e2: C).(\lambda (u: T).(drop n0 n0 (CHead c (Flat f) u2)
+(CHead e2 (Flat f0) u)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2:
+C).(\lambda (_: T).(csubst0 n0 v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f0:
+F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq C
+(CHead c (Flat f) u1) (CHead e1 (Flat f0) u))))))) (\lambda (f0: F).(\lambda
+(_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(drop n0 n0 (CHead c
+(Flat f) u2) (CHead e2 (Flat f0) w))))))) (\lambda (_: F).(\lambda (_:
+C).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 n0 v0 u w))))))
(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
-(_: T).(csubst0 O v0 e1 e2)))))))))) \to (\forall (u: T).((eq nat (s k0 i) O)
-\to (or4 (drop O O (CHead c4 k0 u) (CHead c3 k0 u)) (ex3_4 F C T T (\lambda
-(f: F).(\lambda (e0: C).(\lambda (u0: T).(\lambda (_: T).(eq C (CHead c3 k0
-u) (CHead e0 (Flat f) u0)))))) (\lambda (f: F).(\lambda (e0: C).(\lambda (_:
-T).(\lambda (w: T).(drop O O (CHead c4 k0 u) (CHead e0 (Flat f) w))))))
-(\lambda (_: F).(\lambda (_: C).(\lambda (u0: T).(\lambda (w: T).(subst0 O v0
-u0 w)))))) (ex3_4 F C C T (\lambda (f: F).(\lambda (e1: C).(\lambda (_:
-C).(\lambda (u0: T).(eq C (CHead c3 k0 u) (CHead e1 (Flat f) u0))))))
-(\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u0: T).(drop O O
-(CHead c4 k0 u) (CHead e2 (Flat f) u0)))))) (\lambda (_: F).(\lambda (e1:
-C).(\lambda (e2: C).(\lambda (_: T).(csubst0 O v0 e1 e2)))))) (ex4_5 F C C T
-T (\lambda (f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u0: T).(\lambda
-(_: T).(eq C (CHead c3 k0 u) (CHead e1 (Flat f) u0))))))) (\lambda (f:
+(_: T).(csubst0 n0 v0 e1 e2))))))))) (or4_intro1 (drop O O (CHead c (Flat f)
+u2) (CHead c (Flat f) u1)) (ex3_4 F C T T (\lambda (f0: F).(\lambda (e0:
+C).(\lambda (u: T).(\lambda (_: T).(eq C (CHead c (Flat f) u1) (CHead e0
+(Flat f0) u)))))) (\lambda (f0: F).(\lambda (e0: C).(\lambda (_: T).(\lambda
+(w: T).(drop O O (CHead c (Flat f) u2) (CHead e0 (Flat f0) w)))))) (\lambda
+(_: F).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 O v0 u w))))))
+(ex3_4 F C C T (\lambda (f0: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u:
+T).(eq C (CHead c (Flat f) u1) (CHead e1 (Flat f0) u)))))) (\lambda (f0:
+F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(drop O O (CHead c (Flat
+f) u2) (CHead e2 (Flat f0) u)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda
+(e2: C).(\lambda (_: T).(csubst0 O v0 e1 e2)))))) (ex4_5 F C C T T (\lambda
+(f0: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq
+C (CHead c (Flat f) u1) (CHead e1 (Flat f0) u))))))) (\lambda (f0:
F).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(drop O O
-(CHead c4 k0 u) (CHead e2 (Flat f) w))))))) (\lambda (_: F).(\lambda (_:
-C).(\lambda (_: C).(\lambda (u0: T).(\lambda (w: T).(subst0 O v0 u0 w))))))
+(CHead c (Flat f) u2) (CHead e2 (Flat f0) w))))))) (\lambda (_: F).(\lambda
+(_: C).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 O v0 u w))))))
(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
-(_: T).(csubst0 O v0 e1 e2))))))))))))))))) (\lambda (b: B).(\lambda (i:
-nat).(\lambda (c3: C).(\lambda (c4: C).(\lambda (v0: T).(\lambda (_: (csubst0
-i v0 c3 c4)).(\lambda (_: (((eq nat i O) \to (or4 (drop O O c4 c3) (ex3_4 F C
-T T (\lambda (f: F).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C c3
+(_: T).(csubst0 O v0 e1 e2))))))) (ex3_4_intro F C T T (\lambda (f0:
+F).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C (CHead c (Flat f)
+u1) (CHead e0 (Flat f0) u)))))) (\lambda (f0: F).(\lambda (e0: C).(\lambda
+(_: T).(\lambda (w: T).(drop O O (CHead c (Flat f) u2) (CHead e0 (Flat f0)
+w)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u: T).(\lambda (w:
+T).(subst0 O v0 u w))))) f c u1 u2 (refl_equal C (CHead c (Flat f) u1))
+(drop_refl (CHead c (Flat f) u2)) H4)) i H3)))))))))) k)) (\lambda (k:
+K).(K_ind (\lambda (k0: K).(\forall (i: nat).(\forall (c3: C).(\forall (c4:
+C).(\forall (v0: T).((csubst0 i v0 c3 c4) \to ((((eq nat i O) \to (or4 (drop
+i i c4 c3) (ex3_4 F C T T (\lambda (f: F).(\lambda (e0: C).(\lambda (u:
+T).(\lambda (_: T).(eq C c3 (CHead e0 (Flat f) u)))))) (\lambda (f:
+F).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(drop i i c4 (CHead e0
+(Flat f) w)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u: T).(\lambda (w:
+T).(subst0 i v0 u w)))))) (ex3_4 F C C T (\lambda (f: F).(\lambda (e1:
+C).(\lambda (_: C).(\lambda (u: T).(eq C c3 (CHead e1 (Flat f) u))))))
+(\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(drop i i c4
+(CHead e2 (Flat f) u)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2:
+C).(\lambda (_: T).(csubst0 i v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f:
+F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq C c3
+(CHead e1 (Flat f) u))))))) (\lambda (f: F).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (_: T).(\lambda (w: T).(drop i i c4 (CHead e2 (Flat f) w)))))))
+(\lambda (_: F).(\lambda (_: C).(\lambda (_: C).(\lambda (u: T).(\lambda (w:
+T).(subst0 i v0 u w)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2:
+C).(\lambda (_: T).(\lambda (_: T).(csubst0 i v0 e1 e2)))))))))) \to (\forall
+(u: T).((eq nat (s k0 i) O) \to (or4 (drop (s k0 i) (s k0 i) (CHead c4 k0 u)
+(CHead c3 k0 u)) (ex3_4 F C T T (\lambda (f: F).(\lambda (e0: C).(\lambda
+(u0: T).(\lambda (_: T).(eq C (CHead c3 k0 u) (CHead e0 (Flat f) u0))))))
+(\lambda (f: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(drop (s k0
+i) (s k0 i) (CHead c4 k0 u) (CHead e0 (Flat f) w)))))) (\lambda (_:
+F).(\lambda (_: C).(\lambda (u0: T).(\lambda (w: T).(subst0 (s k0 i) v0 u0
+w)))))) (ex3_4 F C C T (\lambda (f: F).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u0: T).(eq C (CHead c3 k0 u) (CHead e1 (Flat f) u0))))))
+(\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u0: T).(drop (s k0
+i) (s k0 i) (CHead c4 k0 u) (CHead e2 (Flat f) u0)))))) (\lambda (_:
+F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (s k0 i) v0 e1
+e2)))))) (ex4_5 F C C T T (\lambda (f: F).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u0: T).(\lambda (_: T).(eq C (CHead c3 k0 u) (CHead e1 (Flat f)
+u0))))))) (\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (_:
+T).(\lambda (w: T).(drop (s k0 i) (s k0 i) (CHead c4 k0 u) (CHead e2 (Flat f)
+w))))))) (\lambda (_: F).(\lambda (_: C).(\lambda (_: C).(\lambda (u0:
+T).(\lambda (w: T).(subst0 (s k0 i) v0 u0 w)))))) (\lambda (_: F).(\lambda
+(e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 (s k0 i) v0
+e1 e2))))))))))))))))) (\lambda (b: B).(\lambda (i: nat).(\lambda (c3:
+C).(\lambda (c4: C).(\lambda (v0: T).(\lambda (_: (csubst0 i v0 c3
+c4)).(\lambda (_: (((eq nat i O) \to (or4 (drop i i c4 c3) (ex3_4 F C T T
+(\lambda (f: F).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C c3
(CHead e0 (Flat f) u)))))) (\lambda (f: F).(\lambda (e0: C).(\lambda (_:
-T).(\lambda (w: T).(drop O O c4 (CHead e0 (Flat f) w)))))) (\lambda (_:
-F).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 O v0 u w))))))
+T).(\lambda (w: T).(drop i i c4 (CHead e0 (Flat f) w)))))) (\lambda (_:
+F).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 i v0 u w))))))
(ex3_4 F C C T (\lambda (f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u:
T).(eq C c3 (CHead e1 (Flat f) u)))))) (\lambda (f: F).(\lambda (_:
-C).(\lambda (e2: C).(\lambda (u: T).(drop O O c4 (CHead e2 (Flat f) u))))))
-(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 O
+C).(\lambda (e2: C).(\lambda (u: T).(drop i i c4 (CHead e2 (Flat f) u))))))
+(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 i
v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f: F).(\lambda (e1: C).(\lambda (_:
C).(\lambda (u: T).(\lambda (_: T).(eq C c3 (CHead e1 (Flat f) u)))))))
(\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w:
-T).(drop O O c4 (CHead e2 (Flat f) w))))))) (\lambda (_: F).(\lambda (_:
-C).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 O v0 u w))))))
+T).(drop i i c4 (CHead e2 (Flat f) w))))))) (\lambda (_: F).(\lambda (_:
+C).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 i v0 u w))))))
(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
-(_: T).(csubst0 O v0 e1 e2))))))))))).(\lambda (u: T).(\lambda (H4: (eq nat
+(_: T).(csubst0 i v0 e1 e2))))))))))).(\lambda (u: T).(\lambda (H4: (eq nat
(S i) O)).(let H5 \def (eq_ind nat (S i) (\lambda (ee: nat).(match ee in nat
return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow
-True])) I O H4) in (False_ind (or4 (drop O O (CHead c4 (Bind b) u) (CHead c3
-(Bind b) u)) (ex3_4 F C T T (\lambda (f: F).(\lambda (e0: C).(\lambda (u0:
-T).(\lambda (_: T).(eq C (CHead c3 (Bind b) u) (CHead e0 (Flat f) u0))))))
-(\lambda (f: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(drop O O
-(CHead c4 (Bind b) u) (CHead e0 (Flat f) w)))))) (\lambda (_: F).(\lambda (_:
-C).(\lambda (u0: T).(\lambda (w: T).(subst0 O v0 u0 w)))))) (ex3_4 F C C T
-(\lambda (f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u0: T).(eq C
-(CHead c3 (Bind b) u) (CHead e1 (Flat f) u0)))))) (\lambda (f: F).(\lambda
-(_: C).(\lambda (e2: C).(\lambda (u0: T).(drop O O (CHead c4 (Bind b) u)
-(CHead e2 (Flat f) u0)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2:
-C).(\lambda (_: T).(csubst0 O v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f:
-F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(eq C
-(CHead c3 (Bind b) u) (CHead e1 (Flat f) u0))))))) (\lambda (f: F).(\lambda
-(_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(drop O O (CHead c4
-(Bind b) u) (CHead e2 (Flat f) w))))))) (\lambda (_: F).(\lambda (_:
-C).(\lambda (_: C).(\lambda (u0: T).(\lambda (w: T).(subst0 O v0 u0 w))))))
-(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
-(_: T).(csubst0 O v0 e1 e2)))))))) H5))))))))))) (\lambda (f: F).(\lambda (i:
-nat).(\lambda (c3: C).(\lambda (c4: C).(\lambda (v0: T).(\lambda (H2:
-(csubst0 i v0 c3 c4)).(\lambda (H3: (((eq nat i O) \to (or4 (drop O O c4 c3)
-(ex3_4 F C T T (\lambda (f0: F).(\lambda (e0: C).(\lambda (u: T).(\lambda (_:
-T).(eq C c3 (CHead e0 (Flat f0) u)))))) (\lambda (f0: F).(\lambda (e0:
-C).(\lambda (_: T).(\lambda (w: T).(drop O O c4 (CHead e0 (Flat f0) w))))))
-(\lambda (_: F).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 O v0
-u w)))))) (ex3_4 F C C T (\lambda (f0: F).(\lambda (e1: C).(\lambda (_:
-C).(\lambda (u: T).(eq C c3 (CHead e1 (Flat f0) u)))))) (\lambda (f0:
-F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(drop O O c4 (CHead e2
-(Flat f0) u)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda
-(_: T).(csubst0 O v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f0: F).(\lambda
-(e1: C).(\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq C c3 (CHead e1
-(Flat f0) u))))))) (\lambda (f0: F).(\lambda (_: C).(\lambda (e2: C).(\lambda
-(_: T).(\lambda (w: T).(drop O O c4 (CHead e2 (Flat f0) w))))))) (\lambda (_:
-F).(\lambda (_: C).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 O
-v0 u w)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
-T).(\lambda (_: T).(csubst0 O v0 e1 e2))))))))))).(\lambda (u: T).(\lambda
-(H4: (eq nat i O)).(let H5 \def (eq_ind nat i (\lambda (n0: nat).((eq nat n0
-O) \to (or4 (drop O O c4 c3) (ex3_4 F C T T (\lambda (f0: F).(\lambda (e0:
-C).(\lambda (u0: T).(\lambda (_: T).(eq C c3 (CHead e0 (Flat f0) u0))))))
-(\lambda (f0: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(drop O O
-c4 (CHead e0 (Flat f0) w)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u0:
-T).(\lambda (w: T).(subst0 O v0 u0 w)))))) (ex3_4 F C C T (\lambda (f0:
-F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u0: T).(eq C c3 (CHead e1 (Flat
-f0) u0)))))) (\lambda (f0: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u0:
-T).(drop O O c4 (CHead e2 (Flat f0) u0)))))) (\lambda (_: F).(\lambda (e1:
-C).(\lambda (e2: C).(\lambda (_: T).(csubst0 O v0 e1 e2)))))) (ex4_5 F C C T
-T (\lambda (f0: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u0: T).(\lambda
-(_: T).(eq C c3 (CHead e1 (Flat f0) u0))))))) (\lambda (f0: F).(\lambda (_:
-C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(drop O O c4 (CHead e2
-(Flat f0) w))))))) (\lambda (_: F).(\lambda (_: C).(\lambda (_: C).(\lambda
-(u0: T).(\lambda (w: T).(subst0 O v0 u0 w)))))) (\lambda (_: F).(\lambda (e1:
-C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 O v0 e1
-e2)))))))))) H3 O H4) in (let H6 \def (eq_ind nat i (\lambda (n0:
-nat).(csubst0 n0 v0 c3 c4)) H2 O H4) in (or4_intro2 (drop O O (CHead c4 (Flat
-f) u) (CHead c3 (Flat f) u)) (ex3_4 F C T T (\lambda (f0: F).(\lambda (e0:
-C).(\lambda (u0: T).(\lambda (_: T).(eq C (CHead c3 (Flat f) u) (CHead e0
-(Flat f0) u0)))))) (\lambda (f0: F).(\lambda (e0: C).(\lambda (_: T).(\lambda
-(w: T).(drop O O (CHead c4 (Flat f) u) (CHead e0 (Flat f0) w)))))) (\lambda
-(_: F).(\lambda (_: C).(\lambda (u0: T).(\lambda (w: T).(subst0 O v0 u0
-w)))))) (ex3_4 F C C T (\lambda (f0: F).(\lambda (e1: C).(\lambda (_:
-C).(\lambda (u0: T).(eq C (CHead c3 (Flat f) u) (CHead e1 (Flat f0) u0))))))
-(\lambda (f0: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u0: T).(drop O O
-(CHead c4 (Flat f) u) (CHead e2 (Flat f0) u0)))))) (\lambda (_: F).(\lambda
-(e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 O v0 e1 e2)))))) (ex4_5 F C
-C T T (\lambda (f0: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u0:
-T).(\lambda (_: T).(eq C (CHead c3 (Flat f) u) (CHead e1 (Flat f0) u0)))))))
-(\lambda (f0: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
-(w: T).(drop O O (CHead c4 (Flat f) u) (CHead e2 (Flat f0) w))))))) (\lambda
-(_: F).(\lambda (_: C).(\lambda (_: C).(\lambda (u0: T).(\lambda (w:
-T).(subst0 O v0 u0 w)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2:
-C).(\lambda (_: T).(\lambda (_: T).(csubst0 O v0 e1 e2))))))) (ex3_4_intro F
-C C T (\lambda (f0: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u0: T).(eq
-C (CHead c3 (Flat f) u) (CHead e1 (Flat f0) u0)))))) (\lambda (f0:
-F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u0: T).(drop O O (CHead c4
-(Flat f) u) (CHead e2 (Flat f0) u0)))))) (\lambda (_: F).(\lambda (e1:
-C).(\lambda (e2: C).(\lambda (_: T).(csubst0 O v0 e1 e2))))) f c3 c4 u
-(refl_equal C (CHead c3 (Flat f) u)) (drop_refl (CHead c4 (Flat f) u))
-H6))))))))))))) k)) (\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i:
-nat).(\forall (v0: T).(\forall (u1: T).(\forall (u2: T).((subst0 i v0 u1 u2)
-\to (\forall (c3: C).(\forall (c4: C).((csubst0 i v0 c3 c4) \to ((((eq nat i
-O) \to (or4 (drop O O c4 c3) (ex3_4 F C T T (\lambda (f: F).(\lambda (e0:
-C).(\lambda (u: T).(\lambda (_: T).(eq C c3 (CHead e0 (Flat f) u))))))
-(\lambda (f: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(drop O O c4
-(CHead e0 (Flat f) w)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u:
-T).(\lambda (w: T).(subst0 O v0 u w)))))) (ex3_4 F C C T (\lambda (f:
-F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(eq C c3 (CHead e1 (Flat
-f) u)))))) (\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u:
-T).(drop O O c4 (CHead e2 (Flat f) u)))))) (\lambda (_: F).(\lambda (e1:
-C).(\lambda (e2: C).(\lambda (_: T).(csubst0 O v0 e1 e2)))))) (ex4_5 F C C T
-T (\lambda (f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(\lambda
-(_: T).(eq C c3 (CHead e1 (Flat f) u))))))) (\lambda (f: F).(\lambda (_:
-C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(drop O O c4 (CHead e2
-(Flat f) w))))))) (\lambda (_: F).(\lambda (_: C).(\lambda (_: C).(\lambda
-(u: T).(\lambda (w: T).(subst0 O v0 u w)))))) (\lambda (_: F).(\lambda (e1:
-C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 O v0 e1
-e2)))))))))) \to ((eq nat (s k0 i) O) \to (or4 (drop O O (CHead c4 k0 u2)
-(CHead c3 k0 u1)) (ex3_4 F C T T (\lambda (f: F).(\lambda (e0: C).(\lambda
-(u: T).(\lambda (_: T).(eq C (CHead c3 k0 u1) (CHead e0 (Flat f) u))))))
-(\lambda (f: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(drop O O
-(CHead c4 k0 u2) (CHead e0 (Flat f) w)))))) (\lambda (_: F).(\lambda (_:
-C).(\lambda (u: T).(\lambda (w: T).(subst0 O v0 u w)))))) (ex3_4 F C C T
-(\lambda (f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(eq C (CHead
-c3 k0 u1) (CHead e1 (Flat f) u)))))) (\lambda (f: F).(\lambda (_: C).(\lambda
-(e2: C).(\lambda (u: T).(drop O O (CHead c4 k0 u2) (CHead e2 (Flat f) u))))))
-(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 O
-v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f: F).(\lambda (e1: C).(\lambda (_:
-C).(\lambda (u: T).(\lambda (_: T).(eq C (CHead c3 k0 u1) (CHead e1 (Flat f)
-u))))))) (\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (_:
-T).(\lambda (w: T).(drop O O (CHead c4 k0 u2) (CHead e2 (Flat f) w)))))))
-(\lambda (_: F).(\lambda (_: C).(\lambda (_: C).(\lambda (u: T).(\lambda (w:
-T).(subst0 O v0 u w)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2:
-C).(\lambda (_: T).(\lambda (_: T).(csubst0 O v0 e1 e2)))))))))))))))))))
-(\lambda (b: B).(\lambda (i: nat).(\lambda (v0: T).(\lambda (u1: T).(\lambda
-(u2: T).(\lambda (_: (subst0 i v0 u1 u2)).(\lambda (c3: C).(\lambda (c4:
-C).(\lambda (_: (csubst0 i v0 c3 c4)).(\lambda (_: (((eq nat i O) \to (or4
-(drop O O c4 c3) (ex3_4 F C T T (\lambda (f: F).(\lambda (e0: C).(\lambda (u:
-T).(\lambda (_: T).(eq C c3 (CHead e0 (Flat f) u)))))) (\lambda (f:
-F).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(drop O O c4 (CHead e0
-(Flat f) w)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u: T).(\lambda (w:
-T).(subst0 O v0 u w)))))) (ex3_4 F C C T (\lambda (f: F).(\lambda (e1:
-C).(\lambda (_: C).(\lambda (u: T).(eq C c3 (CHead e1 (Flat f) u))))))
-(\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(drop O O c4
-(CHead e2 (Flat f) u)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2:
-C).(\lambda (_: T).(csubst0 O v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f:
-F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq C c3
-(CHead e1 (Flat f) u))))))) (\lambda (f: F).(\lambda (_: C).(\lambda (e2:
-C).(\lambda (_: T).(\lambda (w: T).(drop O O c4 (CHead e2 (Flat f) w)))))))
-(\lambda (_: F).(\lambda (_: C).(\lambda (_: C).(\lambda (u: T).(\lambda (w:
-T).(subst0 O v0 u w)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2:
-C).(\lambda (_: T).(\lambda (_: T).(csubst0 O v0 e1 e2))))))))))).(\lambda
-(H5: (eq nat (S i) O)).(let H6 \def (eq_ind nat (S i) (\lambda (ee:
-nat).(match ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow
-False | (S _) \Rightarrow True])) I O H5) in (False_ind (or4 (drop O O (CHead
-c4 (Bind b) u2) (CHead c3 (Bind b) u1)) (ex3_4 F C T T (\lambda (f:
-F).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C (CHead c3 (Bind b)
-u1) (CHead e0 (Flat f) u)))))) (\lambda (f: F).(\lambda (e0: C).(\lambda (_:
-T).(\lambda (w: T).(drop O O (CHead c4 (Bind b) u2) (CHead e0 (Flat f)
-w)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u: T).(\lambda (w:
-T).(subst0 O v0 u w)))))) (ex3_4 F C C T (\lambda (f: F).(\lambda (e1:
-C).(\lambda (_: C).(\lambda (u: T).(eq C (CHead c3 (Bind b) u1) (CHead e1
-(Flat f) u)))))) (\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda
-(u: T).(drop O O (CHead c4 (Bind b) u2) (CHead e2 (Flat f) u)))))) (\lambda
-(_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 O v0 e1
+True])) I O H4) in (False_ind (or4 (drop (S i) (S i) (CHead c4 (Bind b) u)
+(CHead c3 (Bind b) u)) (ex3_4 F C T T (\lambda (f: F).(\lambda (e0:
+C).(\lambda (u0: T).(\lambda (_: T).(eq C (CHead c3 (Bind b) u) (CHead e0
+(Flat f) u0)))))) (\lambda (f: F).(\lambda (e0: C).(\lambda (_: T).(\lambda
+(w: T).(drop (S i) (S i) (CHead c4 (Bind b) u) (CHead e0 (Flat f) w))))))
+(\lambda (_: F).(\lambda (_: C).(\lambda (u0: T).(\lambda (w: T).(subst0 (S
+i) v0 u0 w)))))) (ex3_4 F C C T (\lambda (f: F).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u0: T).(eq C (CHead c3 (Bind b) u) (CHead e1 (Flat f) u0))))))
+(\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u0: T).(drop (S i)
+(S i) (CHead c4 (Bind b) u) (CHead e2 (Flat f) u0)))))) (\lambda (_:
+F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (S i) v0 e1
e2)))))) (ex4_5 F C C T T (\lambda (f: F).(\lambda (e1: C).(\lambda (_:
-C).(\lambda (u: T).(\lambda (_: T).(eq C (CHead c3 (Bind b) u1) (CHead e1
-(Flat f) u))))))) (\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda
-(_: T).(\lambda (w: T).(drop O O (CHead c4 (Bind b) u2) (CHead e2 (Flat f)
-w))))))) (\lambda (_: F).(\lambda (_: C).(\lambda (_: C).(\lambda (u:
-T).(\lambda (w: T).(subst0 O v0 u w)))))) (\lambda (_: F).(\lambda (e1:
-C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 O v0 e1
-e2)))))))) H6))))))))))))) (\lambda (f: F).(\lambda (i: nat).(\lambda (v0:
-T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (H2: (subst0 i v0 u1
-u2)).(\lambda (c3: C).(\lambda (c4: C).(\lambda (H3: (csubst0 i v0 c3
-c4)).(\lambda (H4: (((eq nat i O) \to (or4 (drop O O c4 c3) (ex3_4 F C T T
+C).(\lambda (u0: T).(\lambda (_: T).(eq C (CHead c3 (Bind b) u) (CHead e1
+(Flat f) u0))))))) (\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda
+(_: T).(\lambda (w: T).(drop (S i) (S i) (CHead c4 (Bind b) u) (CHead e2
+(Flat f) w))))))) (\lambda (_: F).(\lambda (_: C).(\lambda (_: C).(\lambda
+(u0: T).(\lambda (w: T).(subst0 (S i) v0 u0 w)))))) (\lambda (_: F).(\lambda
+(e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 (S i) v0 e1
+e2)))))))) H5))))))))))) (\lambda (f: F).(\lambda (i: nat).(\lambda (c3:
+C).(\lambda (c4: C).(\lambda (v0: T).(\lambda (H2: (csubst0 i v0 c3
+c4)).(\lambda (H3: (((eq nat i O) \to (or4 (drop i i c4 c3) (ex3_4 F C T T
(\lambda (f0: F).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C c3
(CHead e0 (Flat f0) u)))))) (\lambda (f0: F).(\lambda (e0: C).(\lambda (_:
-T).(\lambda (w: T).(drop O O c4 (CHead e0 (Flat f0) w)))))) (\lambda (_:
-F).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 O v0 u w))))))
+T).(\lambda (w: T).(drop i i c4 (CHead e0 (Flat f0) w)))))) (\lambda (_:
+F).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 i v0 u w))))))
(ex3_4 F C C T (\lambda (f0: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u:
T).(eq C c3 (CHead e1 (Flat f0) u)))))) (\lambda (f0: F).(\lambda (_:
-C).(\lambda (e2: C).(\lambda (u: T).(drop O O c4 (CHead e2 (Flat f0) u))))))
-(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 O
+C).(\lambda (e2: C).(\lambda (u: T).(drop i i c4 (CHead e2 (Flat f0) u))))))
+(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 i
v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f0: F).(\lambda (e1: C).(\lambda
(_: C).(\lambda (u: T).(\lambda (_: T).(eq C c3 (CHead e1 (Flat f0) u)))))))
(\lambda (f0: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
-(w: T).(drop O O c4 (CHead e2 (Flat f0) w))))))) (\lambda (_: F).(\lambda (_:
-C).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 O v0 u w))))))
+(w: T).(drop i i c4 (CHead e2 (Flat f0) w))))))) (\lambda (_: F).(\lambda (_:
+C).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 i v0 u w))))))
(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
-(_: T).(csubst0 O v0 e1 e2))))))))))).(\lambda (H5: (eq nat i O)).(let H6
-\def (eq_ind nat i (\lambda (n0: nat).((eq nat n0 O) \to (or4 (drop O O c4
-c3) (ex3_4 F C T T (\lambda (f0: F).(\lambda (e0: C).(\lambda (u: T).(\lambda
-(_: T).(eq C c3 (CHead e0 (Flat f0) u)))))) (\lambda (f0: F).(\lambda (e0:
-C).(\lambda (_: T).(\lambda (w: T).(drop O O c4 (CHead e0 (Flat f0) w))))))
-(\lambda (_: F).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 O v0
-u w)))))) (ex3_4 F C C T (\lambda (f0: F).(\lambda (e1: C).(\lambda (_:
-C).(\lambda (u: T).(eq C c3 (CHead e1 (Flat f0) u)))))) (\lambda (f0:
-F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(drop O O c4 (CHead e2
-(Flat f0) u)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda
-(_: T).(csubst0 O v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f0: F).(\lambda
-(e1: C).(\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq C c3 (CHead e1
-(Flat f0) u))))))) (\lambda (f0: F).(\lambda (_: C).(\lambda (e2: C).(\lambda
-(_: T).(\lambda (w: T).(drop O O c4 (CHead e2 (Flat f0) w))))))) (\lambda (_:
-F).(\lambda (_: C).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 O
-v0 u w)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
-T).(\lambda (_: T).(csubst0 O v0 e1 e2)))))))))) H4 O H5) in (let H7 \def
+(_: T).(csubst0 i v0 e1 e2))))))))))).(\lambda (u: T).(\lambda (H4: (eq nat i
+O)).(let H5 \def (eq_ind nat i (\lambda (n0: nat).((eq nat n0 O) \to (or4
+(drop n0 n0 c4 c3) (ex3_4 F C T T (\lambda (f0: F).(\lambda (e0: C).(\lambda
+(u0: T).(\lambda (_: T).(eq C c3 (CHead e0 (Flat f0) u0)))))) (\lambda (f0:
+F).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(drop n0 n0 c4 (CHead e0
+(Flat f0) w)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u0: T).(\lambda
+(w: T).(subst0 n0 v0 u0 w)))))) (ex3_4 F C C T (\lambda (f0: F).(\lambda (e1:
+C).(\lambda (_: C).(\lambda (u0: T).(eq C c3 (CHead e1 (Flat f0) u0))))))
+(\lambda (f0: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u0: T).(drop n0
+n0 c4 (CHead e2 (Flat f0) u0)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda
+(e2: C).(\lambda (_: T).(csubst0 n0 v0 e1 e2)))))) (ex4_5 F C C T T (\lambda
+(f0: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(eq
+C c3 (CHead e1 (Flat f0) u0))))))) (\lambda (f0: F).(\lambda (_: C).(\lambda
+(e2: C).(\lambda (_: T).(\lambda (w: T).(drop n0 n0 c4 (CHead e2 (Flat f0)
+w))))))) (\lambda (_: F).(\lambda (_: C).(\lambda (_: C).(\lambda (u0:
+T).(\lambda (w: T).(subst0 n0 v0 u0 w)))))) (\lambda (_: F).(\lambda (e1:
+C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 n0 v0 e1
+e2)))))))))) H3 O H4) in (let H6 \def (eq_ind nat i (\lambda (n0:
+nat).(csubst0 n0 v0 c3 c4)) H2 O H4) in (eq_ind_r nat O (\lambda (n0:
+nat).(or4 (drop n0 n0 (CHead c4 (Flat f) u) (CHead c3 (Flat f) u)) (ex3_4 F C
+T T (\lambda (f0: F).(\lambda (e0: C).(\lambda (u0: T).(\lambda (_: T).(eq C
+(CHead c3 (Flat f) u) (CHead e0 (Flat f0) u0)))))) (\lambda (f0: F).(\lambda
+(e0: C).(\lambda (_: T).(\lambda (w: T).(drop n0 n0 (CHead c4 (Flat f) u)
+(CHead e0 (Flat f0) w)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u0:
+T).(\lambda (w: T).(subst0 n0 v0 u0 w)))))) (ex3_4 F C C T (\lambda (f0:
+F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u0: T).(eq C (CHead c3 (Flat f)
+u) (CHead e1 (Flat f0) u0)))))) (\lambda (f0: F).(\lambda (_: C).(\lambda
+(e2: C).(\lambda (u0: T).(drop n0 n0 (CHead c4 (Flat f) u) (CHead e2 (Flat
+f0) u0)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
+T).(csubst0 n0 v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f0: F).(\lambda (e1:
+C).(\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(eq C (CHead c3 (Flat f)
+u) (CHead e1 (Flat f0) u0))))))) (\lambda (f0: F).(\lambda (_: C).(\lambda
+(e2: C).(\lambda (_: T).(\lambda (w: T).(drop n0 n0 (CHead c4 (Flat f) u)
+(CHead e2 (Flat f0) w))))))) (\lambda (_: F).(\lambda (_: C).(\lambda (_:
+C).(\lambda (u0: T).(\lambda (w: T).(subst0 n0 v0 u0 w)))))) (\lambda (_:
+F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0
+n0 v0 e1 e2))))))))) (or4_intro2 (drop O O (CHead c4 (Flat f) u) (CHead c3
+(Flat f) u)) (ex3_4 F C T T (\lambda (f0: F).(\lambda (e0: C).(\lambda (u0:
+T).(\lambda (_: T).(eq C (CHead c3 (Flat f) u) (CHead e0 (Flat f0) u0))))))
+(\lambda (f0: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(drop O O
+(CHead c4 (Flat f) u) (CHead e0 (Flat f0) w)))))) (\lambda (_: F).(\lambda
+(_: C).(\lambda (u0: T).(\lambda (w: T).(subst0 O v0 u0 w)))))) (ex3_4 F C C
+T (\lambda (f0: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u0: T).(eq C
+(CHead c3 (Flat f) u) (CHead e1 (Flat f0) u0)))))) (\lambda (f0: F).(\lambda
+(_: C).(\lambda (e2: C).(\lambda (u0: T).(drop O O (CHead c4 (Flat f) u)
+(CHead e2 (Flat f0) u0)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2:
+C).(\lambda (_: T).(csubst0 O v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f0:
+F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(eq C
+(CHead c3 (Flat f) u) (CHead e1 (Flat f0) u0))))))) (\lambda (f0: F).(\lambda
+(_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(drop O O (CHead c4
+(Flat f) u) (CHead e2 (Flat f0) w))))))) (\lambda (_: F).(\lambda (_:
+C).(\lambda (_: C).(\lambda (u0: T).(\lambda (w: T).(subst0 O v0 u0 w))))))
+(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
+(_: T).(csubst0 O v0 e1 e2))))))) (ex3_4_intro F C C T (\lambda (f0:
+F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u0: T).(eq C (CHead c3 (Flat f)
+u) (CHead e1 (Flat f0) u0)))))) (\lambda (f0: F).(\lambda (_: C).(\lambda
+(e2: C).(\lambda (u0: T).(drop O O (CHead c4 (Flat f) u) (CHead e2 (Flat f0)
+u0)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
+T).(csubst0 O v0 e1 e2))))) f c3 c4 u (refl_equal C (CHead c3 (Flat f) u))
+(drop_refl (CHead c4 (Flat f) u)) H6)) i H4)))))))))))) k)) (\lambda (k:
+K).(K_ind (\lambda (k0: K).(\forall (i: nat).(\forall (v0: T).(\forall (u1:
+T).(\forall (u2: T).((subst0 i v0 u1 u2) \to (\forall (c3: C).(\forall (c4:
+C).((csubst0 i v0 c3 c4) \to ((((eq nat i O) \to (or4 (drop i i c4 c3) (ex3_4
+F C T T (\lambda (f: F).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq
+C c3 (CHead e0 (Flat f) u)))))) (\lambda (f: F).(\lambda (e0: C).(\lambda (_:
+T).(\lambda (w: T).(drop i i c4 (CHead e0 (Flat f) w)))))) (\lambda (_:
+F).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 i v0 u w))))))
+(ex3_4 F C C T (\lambda (f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u:
+T).(eq C c3 (CHead e1 (Flat f) u)))))) (\lambda (f: F).(\lambda (_:
+C).(\lambda (e2: C).(\lambda (u: T).(drop i i c4 (CHead e2 (Flat f) u))))))
+(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 i
+v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f: F).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (_: T).(eq C c3 (CHead e1 (Flat f) u)))))))
+(\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w:
+T).(drop i i c4 (CHead e2 (Flat f) w))))))) (\lambda (_: F).(\lambda (_:
+C).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 i v0 u w))))))
+(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
+(_: T).(csubst0 i v0 e1 e2)))))))))) \to ((eq nat (s k0 i) O) \to (or4 (drop
+(s k0 i) (s k0 i) (CHead c4 k0 u2) (CHead c3 k0 u1)) (ex3_4 F C T T (\lambda
+(f: F).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C (CHead c3 k0
+u1) (CHead e0 (Flat f) u)))))) (\lambda (f: F).(\lambda (e0: C).(\lambda (_:
+T).(\lambda (w: T).(drop (s k0 i) (s k0 i) (CHead c4 k0 u2) (CHead e0 (Flat
+f) w)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u: T).(\lambda (w:
+T).(subst0 (s k0 i) v0 u w)))))) (ex3_4 F C C T (\lambda (f: F).(\lambda (e1:
+C).(\lambda (_: C).(\lambda (u: T).(eq C (CHead c3 k0 u1) (CHead e1 (Flat f)
+u)))))) (\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u:
+T).(drop (s k0 i) (s k0 i) (CHead c4 k0 u2) (CHead e2 (Flat f) u))))))
+(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (s
+k0 i) v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f: F).(\lambda (e1:
+C).(\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq C (CHead c3 k0 u1)
+(CHead e1 (Flat f) u))))))) (\lambda (f: F).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (_: T).(\lambda (w: T).(drop (s k0 i) (s k0 i) (CHead c4 k0 u2)
+(CHead e2 (Flat f) w))))))) (\lambda (_: F).(\lambda (_: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (w: T).(subst0 (s k0 i) v0 u w)))))) (\lambda (_:
+F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0
+(s k0 i) v0 e1 e2))))))))))))))))))) (\lambda (b: B).(\lambda (i:
+nat).(\lambda (v0: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (subst0
+i v0 u1 u2)).(\lambda (c3: C).(\lambda (c4: C).(\lambda (_: (csubst0 i v0 c3
+c4)).(\lambda (_: (((eq nat i O) \to (or4 (drop i i c4 c3) (ex3_4 F C T T
+(\lambda (f: F).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C c3
+(CHead e0 (Flat f) u)))))) (\lambda (f: F).(\lambda (e0: C).(\lambda (_:
+T).(\lambda (w: T).(drop i i c4 (CHead e0 (Flat f) w)))))) (\lambda (_:
+F).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 i v0 u w))))))
+(ex3_4 F C C T (\lambda (f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u:
+T).(eq C c3 (CHead e1 (Flat f) u)))))) (\lambda (f: F).(\lambda (_:
+C).(\lambda (e2: C).(\lambda (u: T).(drop i i c4 (CHead e2 (Flat f) u))))))
+(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 i
+v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f: F).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (_: T).(eq C c3 (CHead e1 (Flat f) u)))))))
+(\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w:
+T).(drop i i c4 (CHead e2 (Flat f) w))))))) (\lambda (_: F).(\lambda (_:
+C).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 i v0 u w))))))
+(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
+(_: T).(csubst0 i v0 e1 e2))))))))))).(\lambda (H5: (eq nat (S i) O)).(let H6
+\def (eq_ind nat (S i) (\lambda (ee: nat).(match ee in nat return (\lambda
+(_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H5)
+in (False_ind (or4 (drop (S i) (S i) (CHead c4 (Bind b) u2) (CHead c3 (Bind
+b) u1)) (ex3_4 F C T T (\lambda (f: F).(\lambda (e0: C).(\lambda (u:
+T).(\lambda (_: T).(eq C (CHead c3 (Bind b) u1) (CHead e0 (Flat f) u))))))
+(\lambda (f: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(drop (S i)
+(S i) (CHead c4 (Bind b) u2) (CHead e0 (Flat f) w)))))) (\lambda (_:
+F).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 (S i) v0 u w))))))
+(ex3_4 F C C T (\lambda (f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u:
+T).(eq C (CHead c3 (Bind b) u1) (CHead e1 (Flat f) u)))))) (\lambda (f:
+F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(drop (S i) (S i) (CHead
+c4 (Bind b) u2) (CHead e2 (Flat f) u)))))) (\lambda (_: F).(\lambda (e1:
+C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (S i) v0 e1 e2)))))) (ex4_5 F C
+C T T (\lambda (f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u:
+T).(\lambda (_: T).(eq C (CHead c3 (Bind b) u1) (CHead e1 (Flat f) u)))))))
+(\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w:
+T).(drop (S i) (S i) (CHead c4 (Bind b) u2) (CHead e2 (Flat f) w)))))))
+(\lambda (_: F).(\lambda (_: C).(\lambda (_: C).(\lambda (u: T).(\lambda (w:
+T).(subst0 (S i) v0 u w)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2:
+C).(\lambda (_: T).(\lambda (_: T).(csubst0 (S i) v0 e1 e2))))))))
+H6))))))))))))) (\lambda (f: F).(\lambda (i: nat).(\lambda (v0: T).(\lambda
+(u1: T).(\lambda (u2: T).(\lambda (H2: (subst0 i v0 u1 u2)).(\lambda (c3:
+C).(\lambda (c4: C).(\lambda (H3: (csubst0 i v0 c3 c4)).(\lambda (H4: (((eq
+nat i O) \to (or4 (drop i i c4 c3) (ex3_4 F C T T (\lambda (f0: F).(\lambda
+(e0: C).(\lambda (u: T).(\lambda (_: T).(eq C c3 (CHead e0 (Flat f0) u))))))
+(\lambda (f0: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (w: T).(drop i i
+c4 (CHead e0 (Flat f0) w)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u:
+T).(\lambda (w: T).(subst0 i v0 u w)))))) (ex3_4 F C C T (\lambda (f0:
+F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(eq C c3 (CHead e1 (Flat
+f0) u)))))) (\lambda (f0: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u:
+T).(drop i i c4 (CHead e2 (Flat f0) u)))))) (\lambda (_: F).(\lambda (e1:
+C).(\lambda (e2: C).(\lambda (_: T).(csubst0 i v0 e1 e2)))))) (ex4_5 F C C T
+T (\lambda (f0: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(\lambda
+(_: T).(eq C c3 (CHead e1 (Flat f0) u))))))) (\lambda (f0: F).(\lambda (_:
+C).(\lambda (e2: C).(\lambda (_: T).(\lambda (w: T).(drop i i c4 (CHead e2
+(Flat f0) w))))))) (\lambda (_: F).(\lambda (_: C).(\lambda (_: C).(\lambda
+(u: T).(\lambda (w: T).(subst0 i v0 u w)))))) (\lambda (_: F).(\lambda (e1:
+C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 i v0 e1
+e2))))))))))).(\lambda (H5: (eq nat i O)).(let H6 \def (eq_ind nat i (\lambda
+(n0: nat).((eq nat n0 O) \to (or4 (drop n0 n0 c4 c3) (ex3_4 F C T T (\lambda
+(f0: F).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C c3 (CHead e0
+(Flat f0) u)))))) (\lambda (f0: F).(\lambda (e0: C).(\lambda (_: T).(\lambda
+(w: T).(drop n0 n0 c4 (CHead e0 (Flat f0) w)))))) (\lambda (_: F).(\lambda
+(_: C).(\lambda (u: T).(\lambda (w: T).(subst0 n0 v0 u w)))))) (ex3_4 F C C T
+(\lambda (f0: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(eq C c3
+(CHead e1 (Flat f0) u)))))) (\lambda (f0: F).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (u: T).(drop n0 n0 c4 (CHead e2 (Flat f0) u)))))) (\lambda (_:
+F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 n0 v0 e1
+e2)))))) (ex4_5 F C C T T (\lambda (f0: F).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u: T).(\lambda (_: T).(eq C c3 (CHead e1 (Flat f0) u)))))))
+(\lambda (f0: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
+(w: T).(drop n0 n0 c4 (CHead e2 (Flat f0) w))))))) (\lambda (_: F).(\lambda
+(_: C).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 n0 v0 u
+w)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
+T).(\lambda (_: T).(csubst0 n0 v0 e1 e2)))))))))) H4 O H5) in (let H7 \def
(eq_ind nat i (\lambda (n0: nat).(csubst0 n0 v0 c3 c4)) H3 O H5) in (let H8
\def (eq_ind nat i (\lambda (n0: nat).(subst0 n0 v0 u1 u2)) H2 O H5) in
-(or4_intro3 (drop O O (CHead c4 (Flat f) u2) (CHead c3 (Flat f) u1)) (ex3_4 F
-C T T (\lambda (f0: F).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C
+(eq_ind_r nat O (\lambda (n0: nat).(or4 (drop n0 n0 (CHead c4 (Flat f) u2)
+(CHead c3 (Flat f) u1)) (ex3_4 F C T T (\lambda (f0: F).(\lambda (e0:
+C).(\lambda (u: T).(\lambda (_: T).(eq C (CHead c3 (Flat f) u1) (CHead e0
+(Flat f0) u)))))) (\lambda (f0: F).(\lambda (e0: C).(\lambda (_: T).(\lambda
+(w: T).(drop n0 n0 (CHead c4 (Flat f) u2) (CHead e0 (Flat f0) w))))))
+(\lambda (_: F).(\lambda (_: C).(\lambda (u: T).(\lambda (w: T).(subst0 n0 v0
+u w)))))) (ex3_4 F C C T (\lambda (f0: F).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u: T).(eq C (CHead c3 (Flat f) u1) (CHead e1 (Flat f0) u))))))
+(\lambda (f0: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(drop n0 n0
+(CHead c4 (Flat f) u2) (CHead e2 (Flat f0) u)))))) (\lambda (_: F).(\lambda
+(e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 n0 v0 e1 e2)))))) (ex4_5 F
+C C T T (\lambda (f0: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u:
+T).(\lambda (_: T).(eq C (CHead c3 (Flat f) u1) (CHead e1 (Flat f0) u)))))))
+(\lambda (f0: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
+(w: T).(drop n0 n0 (CHead c4 (Flat f) u2) (CHead e2 (Flat f0) w)))))))
+(\lambda (_: F).(\lambda (_: C).(\lambda (_: C).(\lambda (u: T).(\lambda (w:
+T).(subst0 n0 v0 u w)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2:
+C).(\lambda (_: T).(\lambda (_: T).(csubst0 n0 v0 e1 e2))))))))) (or4_intro3
+(drop O O (CHead c4 (Flat f) u2) (CHead c3 (Flat f) u1)) (ex3_4 F C T T
+(\lambda (f0: F).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C
(CHead c3 (Flat f) u1) (CHead e0 (Flat f0) u)))))) (\lambda (f0: F).(\lambda
(e0: C).(\lambda (_: T).(\lambda (w: T).(drop O O (CHead c4 (Flat f) u2)
(CHead e0 (Flat f0) w)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u:
C).(\lambda (u: T).(\lambda (w: T).(subst0 O v0 u w)))))) (\lambda (_:
F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0
O v0 e1 e2)))))) f c3 c4 u1 u2 (refl_equal C (CHead c3 (Flat f) u1))
-(drop_refl (CHead c4 (Flat f) u2)) H8 H7)))))))))))))))) k)) y v c1 c2 H1)))
-H) e (drop_gen_refl c1 e H0)))))))) (\lambda (n0: nat).(\lambda (IHn:
+(drop_refl (CHead c4 (Flat f) u2)) H8 H7)) i H5))))))))))))))) k)) y v c1 c2
+H1))) H) e (drop_gen_refl c1 e H0)))))))) (\lambda (n0: nat).(\lambda (IHn:
((\forall (c1: C).(\forall (c2: C).(\forall (v: T).((csubst0 n0 v c1 c2) \to
(\forall (e: C).((drop n0 O c1 e) \to (or4 (drop n0 O c2 e) (ex3_4 F C T T
(\lambda (f: F).(\lambda (e0: C).(\lambda (u: T).(\lambda (_: T).(eq C e
(_: 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))))))))) (insert_eq nat O (\lambda (n0: nat).(csubst0 n0 v c1 c2))
-(or4 (drop O O c1 c2) (ex3_4 F C T T (\lambda (f: F).(\lambda (e0:
-C).(\lambda (_: T).(\lambda (u2: T).(eq C c2 (CHead e0 (Flat f) u2))))))
-(\lambda (f: F).(\lambda (e0: C).(\lambda (u1: T).(\lambda (_: T).(drop O O
-c1 (CHead e0 (Flat f) u1)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u1:
-T).(\lambda (u2: T).(subst0 O v u1 u2)))))) (ex3_4 F C C T (\lambda (f:
-F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(eq C c2 (CHead e2 (Flat
-f) u)))))) (\lambda (f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u:
-T).(drop O O c1 (CHead e1 (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 (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
-(u2: T).(eq C c2 (CHead e2 (Flat f) u2))))))) (\lambda (f: F).(\lambda (e1:
-C).(\lambda (_: C).(\lambda (u1: T).(\lambda (_: T).(drop O O c1 (CHead e1
-(Flat f) 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 (y: nat).(\lambda (H1: (csubst0 y v c1 c2)).(csubst0_ind
-(\lambda (n0: nat).(\lambda (t: T).(\lambda (c: C).(\lambda (c0: C).((eq nat
-n0 O) \to (or4 (drop O O c c0) (ex3_4 F C T T (\lambda (f: F).(\lambda (e0:
-C).(\lambda (_: T).(\lambda (u2: T).(eq C c0 (CHead e0 (Flat f) u2))))))
-(\lambda (f: F).(\lambda (e0: C).(\lambda (u1: T).(\lambda (_: T).(drop O O c
-(CHead e0 (Flat f) u1)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u1:
-T).(\lambda (u2: T).(subst0 O t u1 u2)))))) (ex3_4 F C C T (\lambda (f:
-F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(eq C c0 (CHead e2 (Flat
-f) u)))))) (\lambda (f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u:
-T).(drop O O c (CHead e1 (Flat f) u)))))) (\lambda (_: F).(\lambda (e1:
-C).(\lambda (e2: C).(\lambda (_: T).(csubst0 O t e1 e2)))))) (ex4_5 F C C T T
-(\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
-(u2: T).(eq C c0 (CHead e2 (Flat f) u2))))))) (\lambda (f: F).(\lambda (e1:
-C).(\lambda (_: C).(\lambda (u1: T).(\lambda (_: T).(drop O O c (CHead e1
-(Flat f) u1))))))) (\lambda (_: F).(\lambda (_: C).(\lambda (_: C).(\lambda
-(u1: T).(\lambda (u2: T).(subst0 O t u1 u2)))))) (\lambda (_: F).(\lambda
-(e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 O t e1
-e2))))))))))))) (\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i:
-nat).(\forall (v0: T).(\forall (u1: T).(\forall (u2: T).((subst0 i v0 u1 u2)
-\to (\forall (c: C).((eq nat (s k0 i) O) \to (or4 (drop O O (CHead c k0 u1)
-(CHead c k0 u2)) (ex3_4 F C T T (\lambda (f: F).(\lambda (e0: C).(\lambda (_:
-T).(\lambda (u4: T).(eq C (CHead c k0 u2) (CHead e0 (Flat f) u4))))))
-(\lambda (f: F).(\lambda (e0: C).(\lambda (u3: T).(\lambda (_: T).(drop O O
-(CHead c k0 u1) (CHead e0 (Flat f) u3)))))) (\lambda (_: F).(\lambda (_:
-C).(\lambda (u3: T).(\lambda (u4: T).(subst0 O v0 u3 u4)))))) (ex3_4 F C C T
-(\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(eq C (CHead
-c k0 u2) (CHead e2 (Flat f) u)))))) (\lambda (f: F).(\lambda (e1: C).(\lambda
-(_: C).(\lambda (u: T).(drop O O (CHead c k0 u1) (CHead e1 (Flat f) u))))))
-(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 O
-v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f: F).(\lambda (_: C).(\lambda (e2:
-C).(\lambda (_: T).(\lambda (u4: T).(eq C (CHead c k0 u2) (CHead e2 (Flat f)
-u4))))))) (\lambda (f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u3:
-T).(\lambda (_: T).(drop O O (CHead c k0 u1) (CHead e1 (Flat f) u3)))))))
-(\lambda (_: F).(\lambda (_: C).(\lambda (_: C).(\lambda (u3: T).(\lambda
-(u4: T).(subst0 O v0 u3 u4)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda
-(e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 O v0 e1 e2))))))))))))))))
-(\lambda (b: B).(\lambda (i: nat).(\lambda (v0: T).(\lambda (u1: T).(\lambda
-(u2: T).(\lambda (_: (subst0 i v0 u1 u2)).(\lambda (c: C).(\lambda (H3: (eq
-nat (S i) O)).(let H4 \def (eq_ind nat (S i) (\lambda (ee: nat).(match ee in
-nat return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _)
-\Rightarrow True])) I O H3) in (False_ind (or4 (drop O O (CHead c (Bind b)
-u1) (CHead c (Bind b) u2)) (ex3_4 F C T T (\lambda (f: F).(\lambda (e0:
-C).(\lambda (_: T).(\lambda (u4: T).(eq C (CHead c (Bind b) u2) (CHead e0
-(Flat f) u4)))))) (\lambda (f: F).(\lambda (e0: C).(\lambda (u3: T).(\lambda
-(_: T).(drop O O (CHead c (Bind b) u1) (CHead e0 (Flat f) u3)))))) (\lambda
-(_: F).(\lambda (_: C).(\lambda (u3: T).(\lambda (u4: T).(subst0 O v0 u3
-u4)))))) (ex3_4 F C C T (\lambda (f: F).(\lambda (_: C).(\lambda (e2:
-C).(\lambda (u: T).(eq C (CHead c (Bind b) u2) (CHead e2 (Flat f) u))))))
-(\lambda (f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(drop O O
-(CHead c (Bind b) u1) (CHead e1 (Flat f) u)))))) (\lambda (_: F).(\lambda
-(e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 O v0 e1 e2)))))) (ex4_5 F C
-C T T (\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (_:
-T).(\lambda (u4: T).(eq C (CHead c (Bind b) u2) (CHead e2 (Flat f) u4)))))))
-(\lambda (f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u3: T).(\lambda
-(_: T).(drop O O (CHead c (Bind b) u1) (CHead e1 (Flat f) u3))))))) (\lambda
-(_: F).(\lambda (_: C).(\lambda (_: C).(\lambda (u3: T).(\lambda (u4:
-T).(subst0 O v0 u3 u4)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2:
-C).(\lambda (_: T).(\lambda (_: T).(csubst0 O v0 e1 e2)))))))) H4))))))))))
-(\lambda (f: F).(\lambda (i: nat).(\lambda (v0: T).(\lambda (u1: T).(\lambda
-(u2: T).(\lambda (H2: (subst0 i v0 u1 u2)).(\lambda (c: C).(\lambda (H3: (eq
-nat i O)).(let H4 \def (eq_ind nat i (\lambda (n0: nat).(subst0 n0 v0 u1 u2))
-H2 O H3) in (or4_intro1 (drop O O (CHead c (Flat f) u1) (CHead c (Flat f)
-u2)) (ex3_4 F C T T (\lambda (f0: F).(\lambda (e0: C).(\lambda (_:
+(\lambda (n0: nat).(or4 (drop n0 n0 c1 c2) (ex3_4 F C T T (\lambda (f:
+F).(\lambda (e0: C).(\lambda (_: T).(\lambda (u2: T).(eq C c2 (CHead e0 (Flat
+f) u2)))))) (\lambda (f: F).(\lambda (e0: C).(\lambda (u1: T).(\lambda (_:
+T).(drop n0 n0 c1 (CHead e0 (Flat f) u1)))))) (\lambda (_: F).(\lambda (_:
+C).(\lambda (u1: T).(\lambda (u2: T).(subst0 n0 v u1 u2)))))) (ex3_4 F C C T
+(\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(eq C c2
+(CHead e2 (Flat f) u)))))) (\lambda (f: F).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u: T).(drop n0 n0 c1 (CHead e1 (Flat f) u)))))) (\lambda (_:
+F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 n0 v e1
+e2)))))) (ex4_5 F C C T T (\lambda (f: F).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (_: T).(\lambda (u2: T).(eq C c2 (CHead e2 (Flat f) u2)))))))
+(\lambda (f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(\lambda
+(_: T).(drop n0 n0 c1 (CHead e1 (Flat f) u1))))))) (\lambda (_: F).(\lambda
+(_: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (u2: T).(subst0 n0 v u1
+u2)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
+T).(\lambda (_: T).(csubst0 n0 v e1 e2))))))))) (\lambda (y: nat).(\lambda
+(H1: (csubst0 y v c1 c2)).(csubst0_ind (\lambda (n0: nat).(\lambda (t:
+T).(\lambda (c: C).(\lambda (c0: C).((eq nat n0 O) \to (or4 (drop n0 n0 c c0)
+(ex3_4 F C T T (\lambda (f: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (u2:
+T).(eq C c0 (CHead e0 (Flat f) u2)))))) (\lambda (f: F).(\lambda (e0:
+C).(\lambda (u1: T).(\lambda (_: T).(drop n0 n0 c (CHead e0 (Flat f) u1))))))
+(\lambda (_: F).(\lambda (_: C).(\lambda (u1: T).(\lambda (u2: T).(subst0 n0
+t u1 u2)))))) (ex3_4 F C C T (\lambda (f: F).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (u: T).(eq C c0 (CHead e2 (Flat f) u)))))) (\lambda (f:
+F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(drop n0 n0 c (CHead e1
+(Flat f) u)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda
+(_: T).(csubst0 n0 t e1 e2)))))) (ex4_5 F C C T T (\lambda (f: F).(\lambda
+(_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (u2: T).(eq C c0 (CHead e2
+(Flat f) u2))))))) (\lambda (f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda
+(u1: T).(\lambda (_: T).(drop n0 n0 c (CHead e1 (Flat f) u1))))))) (\lambda
+(_: F).(\lambda (_: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (u2:
+T).(subst0 n0 t u1 u2)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2:
+C).(\lambda (_: T).(\lambda (_: T).(csubst0 n0 t e1 e2))))))))))))) (\lambda
+(k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(\forall (v0: T).(\forall
+(u1: T).(\forall (u2: T).((subst0 i v0 u1 u2) \to (\forall (c: C).((eq nat (s
+k0 i) O) \to (or4 (drop (s k0 i) (s k0 i) (CHead c k0 u1) (CHead c k0 u2))
+(ex3_4 F C T T (\lambda (f: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (u4:
+T).(eq C (CHead c k0 u2) (CHead e0 (Flat f) u4)))))) (\lambda (f: F).(\lambda
+(e0: C).(\lambda (u3: T).(\lambda (_: T).(drop (s k0 i) (s k0 i) (CHead c k0
+u1) (CHead e0 (Flat f) u3)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u3:
+T).(\lambda (u4: T).(subst0 (s k0 i) v0 u3 u4)))))) (ex3_4 F C C T (\lambda
+(f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(eq C (CHead c k0 u2)
+(CHead e2 (Flat f) u)))))) (\lambda (f: F).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u: T).(drop (s k0 i) (s k0 i) (CHead c k0 u1) (CHead e1 (Flat f)
+u)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
+T).(csubst0 (s k0 i) v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f: F).(\lambda
+(_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (u4: T).(eq C (CHead c k0
+u2) (CHead e2 (Flat f) u4))))))) (\lambda (f: F).(\lambda (e1: C).(\lambda
+(_: C).(\lambda (u3: T).(\lambda (_: T).(drop (s k0 i) (s k0 i) (CHead c k0
+u1) (CHead e1 (Flat f) u3))))))) (\lambda (_: F).(\lambda (_: C).(\lambda (_:
+C).(\lambda (u3: T).(\lambda (u4: T).(subst0 (s k0 i) v0 u3 u4)))))) (\lambda
+(_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_:
+T).(csubst0 (s k0 i) v0 e1 e2)))))))))))))))) (\lambda (b: B).(\lambda (i:
+nat).(\lambda (v0: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (subst0
+i v0 u1 u2)).(\lambda (c: C).(\lambda (H3: (eq nat (S i) O)).(let H4 \def
+(eq_ind nat (S i) (\lambda (ee: nat).(match ee in nat return (\lambda (_:
+nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H3) in
+(False_ind (or4 (drop (S i) (S i) (CHead c (Bind b) u1) (CHead c (Bind b)
+u2)) (ex3_4 F C T T (\lambda (f: F).(\lambda (e0: C).(\lambda (_: T).(\lambda
+(u4: T).(eq C (CHead c (Bind b) u2) (CHead e0 (Flat f) u4)))))) (\lambda (f:
+F).(\lambda (e0: C).(\lambda (u3: T).(\lambda (_: T).(drop (S i) (S i) (CHead
+c (Bind b) u1) (CHead e0 (Flat f) u3)))))) (\lambda (_: F).(\lambda (_:
+C).(\lambda (u3: T).(\lambda (u4: T).(subst0 (S i) v0 u3 u4)))))) (ex3_4 F C
+C T (\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(eq C
+(CHead c (Bind b) u2) (CHead e2 (Flat f) u)))))) (\lambda (f: F).(\lambda
+(e1: C).(\lambda (_: C).(\lambda (u: T).(drop (S i) (S i) (CHead c (Bind b)
+u1) (CHead e1 (Flat f) u)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2:
+C).(\lambda (_: T).(csubst0 (S i) v0 e1 e2)))))) (ex4_5 F C C T T (\lambda
+(f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (u4: T).(eq
+C (CHead c (Bind b) u2) (CHead e2 (Flat f) u4))))))) (\lambda (f: F).(\lambda
+(e1: C).(\lambda (_: C).(\lambda (u3: T).(\lambda (_: T).(drop (S i) (S i)
+(CHead c (Bind b) u1) (CHead e1 (Flat f) u3))))))) (\lambda (_: F).(\lambda
+(_: C).(\lambda (_: C).(\lambda (u3: T).(\lambda (u4: T).(subst0 (S i) v0 u3
+u4)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
+T).(\lambda (_: T).(csubst0 (S i) v0 e1 e2)))))))) H4)))))))))) (\lambda (f:
+F).(\lambda (i: nat).(\lambda (v0: T).(\lambda (u1: T).(\lambda (u2:
+T).(\lambda (H2: (subst0 i v0 u1 u2)).(\lambda (c: C).(\lambda (H3: (eq nat i
+O)).(let H4 \def (eq_ind nat i (\lambda (n0: nat).(subst0 n0 v0 u1 u2)) H2 O
+H3) in (eq_ind_r nat O (\lambda (n0: nat).(or4 (drop n0 n0 (CHead c (Flat f)
+u1) (CHead c (Flat f) u2)) (ex3_4 F C T T (\lambda (f0: F).(\lambda (e0:
+C).(\lambda (_: T).(\lambda (u4: T).(eq C (CHead c (Flat f) u2) (CHead e0
+(Flat f0) u4)))))) (\lambda (f0: F).(\lambda (e0: C).(\lambda (u3:
+T).(\lambda (_: T).(drop n0 n0 (CHead c (Flat f) u1) (CHead e0 (Flat f0)
+u3)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u3: T).(\lambda (u4:
+T).(subst0 n0 v0 u3 u4)))))) (ex3_4 F C C T (\lambda (f0: F).(\lambda (_:
+C).(\lambda (e2: C).(\lambda (u: T).(eq C (CHead c (Flat f) u2) (CHead e2
+(Flat f0) u)))))) (\lambda (f0: F).(\lambda (e1: C).(\lambda (_: C).(\lambda
+(u: T).(drop n0 n0 (CHead c (Flat f) u1) (CHead e1 (Flat f0) u)))))) (\lambda
+(_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 n0 v0 e1
+e2)))))) (ex4_5 F C C T T (\lambda (f0: F).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (_: T).(\lambda (u4: T).(eq C (CHead c (Flat f) u2) (CHead e2
+(Flat f0) u4))))))) (\lambda (f0: F).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u3: T).(\lambda (_: T).(drop n0 n0 (CHead c (Flat f) u1) (CHead
+e1 (Flat f0) u3))))))) (\lambda (_: F).(\lambda (_: C).(\lambda (_:
+C).(\lambda (u3: T).(\lambda (u4: T).(subst0 n0 v0 u3 u4)))))) (\lambda (_:
+F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0
+n0 v0 e1 e2))))))))) (or4_intro1 (drop O O (CHead c (Flat f) u1) (CHead c
+(Flat f) u2)) (ex3_4 F C T T (\lambda (f0: F).(\lambda (e0: C).(\lambda (_:
T).(\lambda (u4: T).(eq C (CHead c (Flat f) u2) (CHead e0 (Flat f0) u4))))))
(\lambda (f0: F).(\lambda (e0: C).(\lambda (u3: T).(\lambda (_: T).(drop O O
(CHead c (Flat f) u1) (CHead e0 (Flat f0) u3)))))) (\lambda (_: F).(\lambda
(u3: T).(\lambda (_: T).(drop O O (CHead c (Flat f) u1) (CHead e0 (Flat f0)
u3)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u3: T).(\lambda (u4:
T).(subst0 O v0 u3 u4))))) f c u1 u2 (refl_equal C (CHead c (Flat f) u2))
-(drop_refl (CHead c (Flat f) u1)) H4))))))))))) k)) (\lambda (k: K).(K_ind
-(\lambda (k0: K).(\forall (i: nat).(\forall (c3: C).(\forall (c4: C).(\forall
-(v0: T).((csubst0 i v0 c3 c4) \to ((((eq nat i O) \to (or4 (drop O O c3 c4)
-(ex3_4 F C T T (\lambda (f: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (u2:
-T).(eq C c4 (CHead e0 (Flat f) u2)))))) (\lambda (f: F).(\lambda (e0:
-C).(\lambda (u1: T).(\lambda (_: T).(drop O O c3 (CHead e0 (Flat f) u1))))))
-(\lambda (_: F).(\lambda (_: C).(\lambda (u1: T).(\lambda (u2: T).(subst0 O
-v0 u1 u2)))))) (ex3_4 F C C T (\lambda (f: F).(\lambda (_: C).(\lambda (e2:
-C).(\lambda (u: T).(eq C c4 (CHead e2 (Flat f) u)))))) (\lambda (f:
-F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(drop O O c3 (CHead e1
-(Flat f) u)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda
-(_: T).(csubst0 O v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f: F).(\lambda
-(_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (u2: T).(eq C c4 (CHead e2
-(Flat f) u2))))))) (\lambda (f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda
-(u1: T).(\lambda (_: T).(drop O O c3 (CHead e1 (Flat f) u1))))))) (\lambda
-(_: F).(\lambda (_: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (u2:
-T).(subst0 O v0 u1 u2)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2:
-C).(\lambda (_: T).(\lambda (_: T).(csubst0 O v0 e1 e2)))))))))) \to (\forall
-(u: T).((eq nat (s k0 i) O) \to (or4 (drop O O (CHead c3 k0 u) (CHead c4 k0
-u)) (ex3_4 F C T T (\lambda (f: F).(\lambda (e0: C).(\lambda (_: T).(\lambda
-(u2: T).(eq C (CHead c4 k0 u) (CHead e0 (Flat f) u2)))))) (\lambda (f:
-F).(\lambda (e0: C).(\lambda (u1: T).(\lambda (_: T).(drop O O (CHead c3 k0
-u) (CHead e0 (Flat f) u1)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u1:
-T).(\lambda (u2: T).(subst0 O v0 u1 u2)))))) (ex3_4 F C C T (\lambda (f:
-F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u0: T).(eq C (CHead c4 k0 u)
-(CHead e2 (Flat f) u0)))))) (\lambda (f: F).(\lambda (e1: C).(\lambda (_:
-C).(\lambda (u0: T).(drop O O (CHead c3 k0 u) (CHead e1 (Flat f) u0))))))
-(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 O
-v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f: F).(\lambda (_: C).(\lambda (e2:
+(drop_refl (CHead c (Flat f) u1)) H4)) i H3)))))))))) k)) (\lambda (k:
+K).(K_ind (\lambda (k0: K).(\forall (i: nat).(\forall (c3: C).(\forall (c4:
+C).(\forall (v0: T).((csubst0 i v0 c3 c4) \to ((((eq nat i O) \to (or4 (drop
+i i c3 c4) (ex3_4 F C T T (\lambda (f: F).(\lambda (e0: C).(\lambda (_:
+T).(\lambda (u2: T).(eq C c4 (CHead e0 (Flat f) u2)))))) (\lambda (f:
+F).(\lambda (e0: C).(\lambda (u1: T).(\lambda (_: T).(drop i i c3 (CHead e0
+(Flat f) u1)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u1: T).(\lambda
+(u2: T).(subst0 i v0 u1 u2)))))) (ex3_4 F C C T (\lambda (f: F).(\lambda (_:
+C).(\lambda (e2: C).(\lambda (u: T).(eq C c4 (CHead e2 (Flat f) u))))))
+(\lambda (f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(drop i i c3
+(CHead e1 (Flat f) u)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2:
+C).(\lambda (_: T).(csubst0 i v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f:
+F).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (u2: T).(eq C c4
+(CHead e2 (Flat f) u2))))))) (\lambda (f: F).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u1: T).(\lambda (_: T).(drop i i c3 (CHead e1 (Flat f) u1)))))))
+(\lambda (_: F).(\lambda (_: C).(\lambda (_: C).(\lambda (u1: T).(\lambda
+(u2: T).(subst0 i v0 u1 u2)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda
+(e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 i v0 e1 e2)))))))))) \to
+(\forall (u: T).((eq nat (s k0 i) O) \to (or4 (drop (s k0 i) (s k0 i) (CHead
+c3 k0 u) (CHead c4 k0 u)) (ex3_4 F C T T (\lambda (f: F).(\lambda (e0:
+C).(\lambda (_: T).(\lambda (u2: T).(eq C (CHead c4 k0 u) (CHead e0 (Flat f)
+u2)))))) (\lambda (f: F).(\lambda (e0: C).(\lambda (u1: T).(\lambda (_:
+T).(drop (s k0 i) (s k0 i) (CHead c3 k0 u) (CHead e0 (Flat f) u1))))))
+(\lambda (_: F).(\lambda (_: C).(\lambda (u1: T).(\lambda (u2: T).(subst0 (s
+k0 i) v0 u1 u2)))))) (ex3_4 F C C T (\lambda (f: F).(\lambda (_: C).(\lambda
+(e2: C).(\lambda (u0: T).(eq C (CHead c4 k0 u) (CHead e2 (Flat f) u0))))))
+(\lambda (f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u0: T).(drop (s k0
+i) (s k0 i) (CHead c3 k0 u) (CHead e1 (Flat f) u0)))))) (\lambda (_:
+F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (s k0 i) v0 e1
+e2)))))) (ex4_5 F C C T T (\lambda (f: F).(\lambda (_: C).(\lambda (e2:
C).(\lambda (_: T).(\lambda (u2: T).(eq C (CHead c4 k0 u) (CHead e2 (Flat f)
u2))))))) (\lambda (f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1:
-T).(\lambda (_: T).(drop O O (CHead c3 k0 u) (CHead e1 (Flat f) u1)))))))
-(\lambda (_: F).(\lambda (_: C).(\lambda (_: C).(\lambda (u1: T).(\lambda
-(u2: T).(subst0 O v0 u1 u2)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda
-(e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 O v0 e1 e2)))))))))))))))))
-(\lambda (b: B).(\lambda (i: nat).(\lambda (c3: C).(\lambda (c4: C).(\lambda
-(v0: T).(\lambda (_: (csubst0 i v0 c3 c4)).(\lambda (_: (((eq nat i O) \to
-(or4 (drop O O c3 c4) (ex3_4 F C T T (\lambda (f: F).(\lambda (e0:
-C).(\lambda (_: T).(\lambda (u2: T).(eq C c4 (CHead e0 (Flat f) u2))))))
-(\lambda (f: F).(\lambda (e0: C).(\lambda (u1: T).(\lambda (_: T).(drop O O
-c3 (CHead e0 (Flat f) u1)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u1:
-T).(\lambda (u2: T).(subst0 O v0 u1 u2)))))) (ex3_4 F C C T (\lambda (f:
-F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(eq C c4 (CHead e2 (Flat
-f) u)))))) (\lambda (f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u:
-T).(drop O O c3 (CHead e1 (Flat f) u)))))) (\lambda (_: F).(\lambda (e1:
-C).(\lambda (e2: C).(\lambda (_: T).(csubst0 O v0 e1 e2)))))) (ex4_5 F C C T
-T (\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
-(u2: T).(eq C c4 (CHead e2 (Flat f) u2))))))) (\lambda (f: F).(\lambda (e1:
-C).(\lambda (_: C).(\lambda (u1: T).(\lambda (_: T).(drop O O c3 (CHead e1
-(Flat f) u1))))))) (\lambda (_: F).(\lambda (_: C).(\lambda (_: C).(\lambda
-(u1: T).(\lambda (u2: T).(subst0 O v0 u1 u2)))))) (\lambda (_: F).(\lambda
-(e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 O v0 e1
-e2))))))))))).(\lambda (u: T).(\lambda (H4: (eq nat (S i) O)).(let H5 \def
-(eq_ind nat (S i) (\lambda (ee: nat).(match ee in nat return (\lambda (_:
-nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H4) in
-(False_ind (or4 (drop O O (CHead c3 (Bind b) u) (CHead c4 (Bind b) u)) (ex3_4
-F C T T (\lambda (f: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (u2: T).(eq
-C (CHead c4 (Bind b) u) (CHead e0 (Flat f) u2)))))) (\lambda (f: F).(\lambda
-(e0: C).(\lambda (u1: T).(\lambda (_: T).(drop O O (CHead c3 (Bind b) u)
-(CHead e0 (Flat f) u1)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u1:
-T).(\lambda (u2: T).(subst0 O v0 u1 u2)))))) (ex3_4 F C C T (\lambda (f:
-F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u0: T).(eq C (CHead c4 (Bind b)
-u) (CHead e2 (Flat f) u0)))))) (\lambda (f: F).(\lambda (e1: C).(\lambda (_:
-C).(\lambda (u0: T).(drop O O (CHead c3 (Bind b) u) (CHead e1 (Flat f)
-u0)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
-T).(csubst0 O v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f: F).(\lambda (_:
-C).(\lambda (e2: C).(\lambda (_: T).(\lambda (u2: T).(eq C (CHead c4 (Bind b)
-u) (CHead e2 (Flat f) u2))))))) (\lambda (f: F).(\lambda (e1: C).(\lambda (_:
-C).(\lambda (u1: T).(\lambda (_: T).(drop O O (CHead c3 (Bind b) u) (CHead e1
-(Flat f) u1))))))) (\lambda (_: F).(\lambda (_: C).(\lambda (_: C).(\lambda
-(u1: T).(\lambda (u2: T).(subst0 O v0 u1 u2)))))) (\lambda (_: F).(\lambda
-(e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 O v0 e1
-e2)))))))) H5))))))))))) (\lambda (f: F).(\lambda (i: nat).(\lambda (c3:
-C).(\lambda (c4: C).(\lambda (v0: T).(\lambda (H2: (csubst0 i v0 c3
-c4)).(\lambda (H3: (((eq nat i O) \to (or4 (drop O O c3 c4) (ex3_4 F C T T
-(\lambda (f0: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (u2: T).(eq C c4
-(CHead e0 (Flat f0) u2)))))) (\lambda (f0: F).(\lambda (e0: C).(\lambda (u1:
-T).(\lambda (_: T).(drop O O c3 (CHead e0 (Flat f0) u1)))))) (\lambda (_:
-F).(\lambda (_: C).(\lambda (u1: T).(\lambda (u2: T).(subst0 O v0 u1 u2))))))
-(ex3_4 F C C T (\lambda (f0: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u:
-T).(eq C c4 (CHead e2 (Flat f0) u)))))) (\lambda (f0: F).(\lambda (e1:
-C).(\lambda (_: C).(\lambda (u: T).(drop O O c3 (CHead e1 (Flat f0) u))))))
-(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 O
-v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f0: F).(\lambda (_: C).(\lambda
-(e2: C).(\lambda (_: T).(\lambda (u2: T).(eq C c4 (CHead e2 (Flat f0)
-u2))))))) (\lambda (f0: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1:
-T).(\lambda (_: T).(drop O O c3 (CHead e1 (Flat f0) u1))))))) (\lambda (_:
-F).(\lambda (_: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (u2: T).(subst0
-O v0 u1 u2)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda
-(_: T).(\lambda (_: T).(csubst0 O v0 e1 e2))))))))))).(\lambda (u:
-T).(\lambda (H4: (eq nat i O)).(let H5 \def (eq_ind nat i (\lambda (n0:
-nat).((eq nat n0 O) \to (or4 (drop O O c3 c4) (ex3_4 F C T T (\lambda (f0:
-F).(\lambda (e0: C).(\lambda (_: T).(\lambda (u2: T).(eq C c4 (CHead e0 (Flat
-f0) u2)))))) (\lambda (f0: F).(\lambda (e0: C).(\lambda (u1: T).(\lambda (_:
-T).(drop O O c3 (CHead e0 (Flat f0) u1)))))) (\lambda (_: F).(\lambda (_:
-C).(\lambda (u1: T).(\lambda (u2: T).(subst0 O v0 u1 u2)))))) (ex3_4 F C C T
-(\lambda (f0: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u0: T).(eq C c4
-(CHead e2 (Flat f0) u0)))))) (\lambda (f0: F).(\lambda (e1: C).(\lambda (_:
-C).(\lambda (u0: T).(drop O O c3 (CHead e1 (Flat f0) u0)))))) (\lambda (_:
-F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 O v0 e1
-e2)))))) (ex4_5 F C C T T (\lambda (f0: F).(\lambda (_: C).(\lambda (e2:
-C).(\lambda (_: T).(\lambda (u2: T).(eq C c4 (CHead e2 (Flat f0) u2)))))))
-(\lambda (f0: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(\lambda
-(_: T).(drop O O c3 (CHead e1 (Flat f0) u1))))))) (\lambda (_: F).(\lambda
-(_: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (u2: T).(subst0 O v0 u1
-u2)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
-T).(\lambda (_: T).(csubst0 O v0 e1 e2)))))))))) H3 O H4) in (let H6 \def
-(eq_ind nat i (\lambda (n0: nat).(csubst0 n0 v0 c3 c4)) H2 O H4) in
-(or4_intro2 (drop O O (CHead c3 (Flat f) u) (CHead c4 (Flat f) u)) (ex3_4 F C
+T).(\lambda (_: T).(drop (s k0 i) (s k0 i) (CHead c3 k0 u) (CHead e1 (Flat f)
+u1))))))) (\lambda (_: F).(\lambda (_: C).(\lambda (_: C).(\lambda (u1:
+T).(\lambda (u2: T).(subst0 (s k0 i) v0 u1 u2)))))) (\lambda (_: F).(\lambda
+(e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 (s k0 i) v0
+e1 e2))))))))))))))))) (\lambda (b: B).(\lambda (i: nat).(\lambda (c3:
+C).(\lambda (c4: C).(\lambda (v0: T).(\lambda (_: (csubst0 i v0 c3
+c4)).(\lambda (_: (((eq nat i O) \to (or4 (drop i i c3 c4) (ex3_4 F C T T
+(\lambda (f: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (u2: T).(eq C c4
+(CHead e0 (Flat f) u2)))))) (\lambda (f: F).(\lambda (e0: C).(\lambda (u1:
+T).(\lambda (_: T).(drop i i c3 (CHead e0 (Flat f) u1)))))) (\lambda (_:
+F).(\lambda (_: C).(\lambda (u1: T).(\lambda (u2: T).(subst0 i v0 u1 u2))))))
+(ex3_4 F C C T (\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u:
+T).(eq C c4 (CHead e2 (Flat f) u)))))) (\lambda (f: F).(\lambda (e1:
+C).(\lambda (_: C).(\lambda (u: T).(drop i i c3 (CHead e1 (Flat f) u))))))
+(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 i
+v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f: F).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (_: T).(\lambda (u2: T).(eq C c4 (CHead e2 (Flat f) u2)))))))
+(\lambda (f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u1: T).(\lambda
+(_: T).(drop i i c3 (CHead e1 (Flat f) u1))))))) (\lambda (_: F).(\lambda (_:
+C).(\lambda (_: C).(\lambda (u1: T).(\lambda (u2: T).(subst0 i v0 u1 u2))))))
+(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
+(_: T).(csubst0 i v0 e1 e2))))))))))).(\lambda (u: T).(\lambda (H4: (eq nat
+(S i) O)).(let H5 \def (eq_ind nat (S i) (\lambda (ee: nat).(match ee in nat
+return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow
+True])) I O H4) in (False_ind (or4 (drop (S i) (S i) (CHead c3 (Bind b) u)
+(CHead c4 (Bind b) u)) (ex3_4 F C T T (\lambda (f: F).(\lambda (e0:
+C).(\lambda (_: T).(\lambda (u2: T).(eq C (CHead c4 (Bind b) u) (CHead e0
+(Flat f) u2)))))) (\lambda (f: F).(\lambda (e0: C).(\lambda (u1: T).(\lambda
+(_: T).(drop (S i) (S i) (CHead c3 (Bind b) u) (CHead e0 (Flat f) u1))))))
+(\lambda (_: F).(\lambda (_: C).(\lambda (u1: T).(\lambda (u2: T).(subst0 (S
+i) v0 u1 u2)))))) (ex3_4 F C C T (\lambda (f: F).(\lambda (_: C).(\lambda
+(e2: C).(\lambda (u0: T).(eq C (CHead c4 (Bind b) u) (CHead e2 (Flat f)
+u0)))))) (\lambda (f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u0:
+T).(drop (S i) (S i) (CHead c3 (Bind b) u) (CHead e1 (Flat f) u0))))))
+(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (S
+i) v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f: F).(\lambda (_: C).(\lambda
+(e2: C).(\lambda (_: T).(\lambda (u2: T).(eq C (CHead c4 (Bind b) u) (CHead
+e2 (Flat f) u2))))))) (\lambda (f: F).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u1: T).(\lambda (_: T).(drop (S i) (S i) (CHead c3 (Bind b) u)
+(CHead e1 (Flat f) u1))))))) (\lambda (_: F).(\lambda (_: C).(\lambda (_:
+C).(\lambda (u1: T).(\lambda (u2: T).(subst0 (S i) v0 u1 u2)))))) (\lambda
+(_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_:
+T).(csubst0 (S i) v0 e1 e2)))))))) H5))))))))))) (\lambda (f: F).(\lambda (i:
+nat).(\lambda (c3: C).(\lambda (c4: C).(\lambda (v0: T).(\lambda (H2:
+(csubst0 i v0 c3 c4)).(\lambda (H3: (((eq nat i O) \to (or4 (drop i i c3 c4)
+(ex3_4 F C T T (\lambda (f0: F).(\lambda (e0: C).(\lambda (_: T).(\lambda
+(u2: T).(eq C c4 (CHead e0 (Flat f0) u2)))))) (\lambda (f0: F).(\lambda (e0:
+C).(\lambda (u1: T).(\lambda (_: T).(drop i i c3 (CHead e0 (Flat f0) u1))))))
+(\lambda (_: F).(\lambda (_: C).(\lambda (u1: T).(\lambda (u2: T).(subst0 i
+v0 u1 u2)))))) (ex3_4 F C C T (\lambda (f0: F).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (u: T).(eq C c4 (CHead e2 (Flat f0) u)))))) (\lambda (f0:
+F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(drop i i c3 (CHead e1
+(Flat f0) u)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda
+(_: T).(csubst0 i v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f0: F).(\lambda
+(_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (u2: T).(eq C c4 (CHead e2
+(Flat f0) u2))))))) (\lambda (f0: F).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u1: T).(\lambda (_: T).(drop i i c3 (CHead e1 (Flat f0)
+u1))))))) (\lambda (_: F).(\lambda (_: C).(\lambda (_: C).(\lambda (u1:
+T).(\lambda (u2: T).(subst0 i v0 u1 u2)))))) (\lambda (_: F).(\lambda (e1:
+C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 i v0 e1
+e2))))))))))).(\lambda (u: T).(\lambda (H4: (eq nat i O)).(let H5 \def
+(eq_ind nat i (\lambda (n0: nat).((eq nat n0 O) \to (or4 (drop n0 n0 c3 c4)
+(ex3_4 F C T T (\lambda (f0: F).(\lambda (e0: C).(\lambda (_: T).(\lambda
+(u2: T).(eq C c4 (CHead e0 (Flat f0) u2)))))) (\lambda (f0: F).(\lambda (e0:
+C).(\lambda (u1: T).(\lambda (_: T).(drop n0 n0 c3 (CHead e0 (Flat f0)
+u1)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u1: T).(\lambda (u2:
+T).(subst0 n0 v0 u1 u2)))))) (ex3_4 F C C T (\lambda (f0: F).(\lambda (_:
+C).(\lambda (e2: C).(\lambda (u0: T).(eq C c4 (CHead e2 (Flat f0) u0))))))
+(\lambda (f0: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u0: T).(drop n0
+n0 c3 (CHead e1 (Flat f0) u0)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda
+(e2: C).(\lambda (_: T).(csubst0 n0 v0 e1 e2)))))) (ex4_5 F C C T T (\lambda
+(f0: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (u2: T).(eq
+C c4 (CHead e2 (Flat f0) u2))))))) (\lambda (f0: F).(\lambda (e1: C).(\lambda
+(_: C).(\lambda (u1: T).(\lambda (_: T).(drop n0 n0 c3 (CHead e1 (Flat f0)
+u1))))))) (\lambda (_: F).(\lambda (_: C).(\lambda (_: C).(\lambda (u1:
+T).(\lambda (u2: T).(subst0 n0 v0 u1 u2)))))) (\lambda (_: F).(\lambda (e1:
+C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 n0 v0 e1
+e2)))))))))) H3 O H4) in (let H6 \def (eq_ind nat i (\lambda (n0:
+nat).(csubst0 n0 v0 c3 c4)) H2 O H4) in (eq_ind_r nat O (\lambda (n0:
+nat).(or4 (drop n0 n0 (CHead c3 (Flat f) u) (CHead c4 (Flat f) u)) (ex3_4 F C
T T (\lambda (f0: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (u2: T).(eq C
(CHead c4 (Flat f) u) (CHead e0 (Flat f0) u2)))))) (\lambda (f0: F).(\lambda
-(e0: C).(\lambda (u1: T).(\lambda (_: T).(drop O O (CHead c3 (Flat f) u)
+(e0: C).(\lambda (u1: T).(\lambda (_: T).(drop n0 n0 (CHead c3 (Flat f) u)
(CHead e0 (Flat f0) u1)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u1:
-T).(\lambda (u2: T).(subst0 O v0 u1 u2)))))) (ex3_4 F C C T (\lambda (f0:
+T).(\lambda (u2: T).(subst0 n0 v0 u1 u2)))))) (ex3_4 F C C T (\lambda (f0:
F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u0: T).(eq C (CHead c4 (Flat f)
u) (CHead e2 (Flat f0) u0)))))) (\lambda (f0: F).(\lambda (e1: C).(\lambda
-(_: C).(\lambda (u0: T).(drop O O (CHead c3 (Flat f) u) (CHead e1 (Flat f0)
+(_: C).(\lambda (u0: T).(drop n0 n0 (CHead c3 (Flat f) u) (CHead e1 (Flat f0)
u0)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
-T).(csubst0 O v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f0: F).(\lambda (_:
+T).(csubst0 n0 v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f0: F).(\lambda (_:
C).(\lambda (e2: C).(\lambda (_: T).(\lambda (u2: T).(eq C (CHead c4 (Flat f)
u) (CHead e2 (Flat f0) u2))))))) (\lambda (f0: F).(\lambda (e1: C).(\lambda
-(_: C).(\lambda (u1: T).(\lambda (_: T).(drop O O (CHead c3 (Flat f) u)
+(_: C).(\lambda (u1: T).(\lambda (_: T).(drop n0 n0 (CHead c3 (Flat f) u)
(CHead e1 (Flat f0) u1))))))) (\lambda (_: F).(\lambda (_: C).(\lambda (_:
-C).(\lambda (u1: T).(\lambda (u2: T).(subst0 O v0 u1 u2)))))) (\lambda (_:
+C).(\lambda (u1: T).(\lambda (u2: T).(subst0 n0 v0 u1 u2)))))) (\lambda (_:
F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0
-O v0 e1 e2))))))) (ex3_4_intro F C C T (\lambda (f0: F).(\lambda (_:
-C).(\lambda (e2: C).(\lambda (u0: T).(eq C (CHead c4 (Flat f) u) (CHead e2
-(Flat f0) u0)))))) (\lambda (f0: F).(\lambda (e1: C).(\lambda (_: C).(\lambda
-(u0: T).(drop O O (CHead c3 (Flat f) u) (CHead e1 (Flat f0) u0)))))) (\lambda
-(_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 O v0 e1
-e2))))) f c3 c4 u (refl_equal C (CHead c4 (Flat f) u)) (drop_refl (CHead c3
-(Flat f) u)) H6))))))))))))) k)) (\lambda (k: K).(K_ind (\lambda (k0:
-K).(\forall (i: nat).(\forall (v0: T).(\forall (u1: T).(\forall (u2:
-T).((subst0 i v0 u1 u2) \to (\forall (c3: C).(\forall (c4: C).((csubst0 i v0
-c3 c4) \to ((((eq nat i O) \to (or4 (drop O O c3 c4) (ex3_4 F C T T (\lambda
-(f: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (u4: T).(eq C c4 (CHead e0
-(Flat f) u4)))))) (\lambda (f: F).(\lambda (e0: C).(\lambda (u3: T).(\lambda
-(_: T).(drop O O c3 (CHead e0 (Flat f) u3)))))) (\lambda (_: F).(\lambda (_:
-C).(\lambda (u3: T).(\lambda (u4: T).(subst0 O v0 u3 u4)))))) (ex3_4 F C C T
-(\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(eq C c4
-(CHead e2 (Flat f) u)))))) (\lambda (f: F).(\lambda (e1: C).(\lambda (_:
-C).(\lambda (u: T).(drop O O c3 (CHead e1 (Flat f) u)))))) (\lambda (_:
-F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 O v0 e1
-e2)))))) (ex4_5 F C C T T (\lambda (f: F).(\lambda (_: C).(\lambda (e2:
+n0 v0 e1 e2))))))))) (or4_intro2 (drop O O (CHead c3 (Flat f) u) (CHead c4
+(Flat f) u)) (ex3_4 F C T T (\lambda (f0: F).(\lambda (e0: C).(\lambda (_:
+T).(\lambda (u2: T).(eq C (CHead c4 (Flat f) u) (CHead e0 (Flat f0) u2))))))
+(\lambda (f0: F).(\lambda (e0: C).(\lambda (u1: T).(\lambda (_: T).(drop O O
+(CHead c3 (Flat f) u) (CHead e0 (Flat f0) u1)))))) (\lambda (_: F).(\lambda
+(_: C).(\lambda (u1: T).(\lambda (u2: T).(subst0 O v0 u1 u2)))))) (ex3_4 F C
+C T (\lambda (f0: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u0: T).(eq C
+(CHead c4 (Flat f) u) (CHead e2 (Flat f0) u0)))))) (\lambda (f0: F).(\lambda
+(e1: C).(\lambda (_: C).(\lambda (u0: T).(drop O O (CHead c3 (Flat f) u)
+(CHead e1 (Flat f0) u0)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2:
+C).(\lambda (_: T).(csubst0 O v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f0:
+F).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (u2: T).(eq C
+(CHead c4 (Flat f) u) (CHead e2 (Flat f0) u2))))))) (\lambda (f0: F).(\lambda
+(e1: C).(\lambda (_: C).(\lambda (u1: T).(\lambda (_: T).(drop O O (CHead c3
+(Flat f) u) (CHead e1 (Flat f0) u1))))))) (\lambda (_: F).(\lambda (_:
+C).(\lambda (_: C).(\lambda (u1: T).(\lambda (u2: T).(subst0 O v0 u1 u2))))))
+(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
+(_: T).(csubst0 O v0 e1 e2))))))) (ex3_4_intro F C C T (\lambda (f0:
+F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u0: T).(eq C (CHead c4 (Flat f)
+u) (CHead e2 (Flat f0) u0)))))) (\lambda (f0: F).(\lambda (e1: C).(\lambda
+(_: C).(\lambda (u0: T).(drop O O (CHead c3 (Flat f) u) (CHead e1 (Flat f0)
+u0)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
+T).(csubst0 O v0 e1 e2))))) f c3 c4 u (refl_equal C (CHead c4 (Flat f) u))
+(drop_refl (CHead c3 (Flat f) u)) H6)) i H4)))))))))))) k)) (\lambda (k:
+K).(K_ind (\lambda (k0: K).(\forall (i: nat).(\forall (v0: T).(\forall (u1:
+T).(\forall (u2: T).((subst0 i v0 u1 u2) \to (\forall (c3: C).(\forall (c4:
+C).((csubst0 i v0 c3 c4) \to ((((eq nat i O) \to (or4 (drop i i c3 c4) (ex3_4
+F C T T (\lambda (f: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (u4: T).(eq
+C c4 (CHead e0 (Flat f) u4)))))) (\lambda (f: F).(\lambda (e0: C).(\lambda
+(u3: T).(\lambda (_: T).(drop i i c3 (CHead e0 (Flat f) u3)))))) (\lambda (_:
+F).(\lambda (_: C).(\lambda (u3: T).(\lambda (u4: T).(subst0 i v0 u3 u4))))))
+(ex3_4 F C C T (\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u:
+T).(eq C c4 (CHead e2 (Flat f) u)))))) (\lambda (f: F).(\lambda (e1:
+C).(\lambda (_: C).(\lambda (u: T).(drop i i c3 (CHead e1 (Flat f) u))))))
+(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 i
+v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f: F).(\lambda (_: C).(\lambda (e2:
C).(\lambda (_: T).(\lambda (u4: T).(eq C c4 (CHead e2 (Flat f) u4)))))))
(\lambda (f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u3: T).(\lambda
-(_: T).(drop O O c3 (CHead e1 (Flat f) u3))))))) (\lambda (_: F).(\lambda (_:
-C).(\lambda (_: C).(\lambda (u3: T).(\lambda (u4: T).(subst0 O v0 u3 u4))))))
+(_: T).(drop i i c3 (CHead e1 (Flat f) u3))))))) (\lambda (_: F).(\lambda (_:
+C).(\lambda (_: C).(\lambda (u3: T).(\lambda (u4: T).(subst0 i v0 u3 u4))))))
(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
-(_: T).(csubst0 O v0 e1 e2)))))))))) \to ((eq nat (s k0 i) O) \to (or4 (drop
-O O (CHead c3 k0 u1) (CHead c4 k0 u2)) (ex3_4 F C T T (\lambda (f:
-F).(\lambda (e0: C).(\lambda (_: T).(\lambda (u4: T).(eq C (CHead c4 k0 u2)
-(CHead e0 (Flat f) u4)))))) (\lambda (f: F).(\lambda (e0: C).(\lambda (u3:
-T).(\lambda (_: T).(drop O O (CHead c3 k0 u1) (CHead e0 (Flat f) u3))))))
-(\lambda (_: F).(\lambda (_: C).(\lambda (u3: T).(\lambda (u4: T).(subst0 O
-v0 u3 u4)))))) (ex3_4 F C C T (\lambda (f: F).(\lambda (_: C).(\lambda (e2:
-C).(\lambda (u: T).(eq C (CHead c4 k0 u2) (CHead e2 (Flat f) u)))))) (\lambda
-(f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(drop O O (CHead c3
-k0 u1) (CHead e1 (Flat f) u)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda
-(e2: C).(\lambda (_: T).(csubst0 O v0 e1 e2)))))) (ex4_5 F C C T T (\lambda
-(f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (u4: T).(eq
-C (CHead c4 k0 u2) (CHead e2 (Flat f) u4))))))) (\lambda (f: F).(\lambda (e1:
-C).(\lambda (_: C).(\lambda (u3: T).(\lambda (_: T).(drop O O (CHead c3 k0
+(_: T).(csubst0 i v0 e1 e2)))))))))) \to ((eq nat (s k0 i) O) \to (or4 (drop
+(s k0 i) (s k0 i) (CHead c3 k0 u1) (CHead c4 k0 u2)) (ex3_4 F C T T (\lambda
+(f: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (u4: T).(eq C (CHead c4 k0
+u2) (CHead e0 (Flat f) u4)))))) (\lambda (f: F).(\lambda (e0: C).(\lambda
+(u3: T).(\lambda (_: T).(drop (s k0 i) (s k0 i) (CHead c3 k0 u1) (CHead e0
+(Flat f) u3)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u3: T).(\lambda
+(u4: T).(subst0 (s k0 i) v0 u3 u4)))))) (ex3_4 F C C T (\lambda (f:
+F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(eq C (CHead c4 k0 u2)
+(CHead e2 (Flat f) u)))))) (\lambda (f: F).(\lambda (e1: C).(\lambda (_:
+C).(\lambda (u: T).(drop (s k0 i) (s k0 i) (CHead c3 k0 u1) (CHead e1 (Flat
+f) u)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_:
+T).(csubst0 (s k0 i) v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f: F).(\lambda
+(_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (u4: T).(eq C (CHead c4 k0
+u2) (CHead e2 (Flat f) u4))))))) (\lambda (f: F).(\lambda (e1: C).(\lambda
+(_: C).(\lambda (u3: T).(\lambda (_: T).(drop (s k0 i) (s k0 i) (CHead c3 k0
u1) (CHead e1 (Flat f) u3))))))) (\lambda (_: F).(\lambda (_: C).(\lambda (_:
-C).(\lambda (u3: T).(\lambda (u4: T).(subst0 O v0 u3 u4)))))) (\lambda (_:
-F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0
-O v0 e1 e2))))))))))))))))))) (\lambda (b: B).(\lambda (i: nat).(\lambda (v0:
-T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (subst0 i v0 u1
-u2)).(\lambda (c3: C).(\lambda (c4: C).(\lambda (_: (csubst0 i v0 c3
-c4)).(\lambda (_: (((eq nat i O) \to (or4 (drop O O c3 c4) (ex3_4 F C T T
+C).(\lambda (u3: T).(\lambda (u4: T).(subst0 (s k0 i) v0 u3 u4)))))) (\lambda
+(_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_:
+T).(csubst0 (s k0 i) v0 e1 e2))))))))))))))))))) (\lambda (b: B).(\lambda (i:
+nat).(\lambda (v0: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (subst0
+i v0 u1 u2)).(\lambda (c3: C).(\lambda (c4: C).(\lambda (_: (csubst0 i v0 c3
+c4)).(\lambda (_: (((eq nat i O) \to (or4 (drop i i c3 c4) (ex3_4 F C T T
(\lambda (f: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (u4: T).(eq C c4
(CHead e0 (Flat f) u4)))))) (\lambda (f: F).(\lambda (e0: C).(\lambda (u3:
-T).(\lambda (_: T).(drop O O c3 (CHead e0 (Flat f) u3)))))) (\lambda (_:
-F).(\lambda (_: C).(\lambda (u3: T).(\lambda (u4: T).(subst0 O v0 u3 u4))))))
+T).(\lambda (_: T).(drop i i c3 (CHead e0 (Flat f) u3)))))) (\lambda (_:
+F).(\lambda (_: C).(\lambda (u3: T).(\lambda (u4: T).(subst0 i v0 u3 u4))))))
(ex3_4 F C C T (\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u:
T).(eq C c4 (CHead e2 (Flat f) u)))))) (\lambda (f: F).(\lambda (e1:
-C).(\lambda (_: C).(\lambda (u: T).(drop O O c3 (CHead e1 (Flat f) u))))))
-(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 O
+C).(\lambda (_: C).(\lambda (u: T).(drop i i c3 (CHead e1 (Flat f) u))))))
+(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 i
v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f: F).(\lambda (_: C).(\lambda (e2:
C).(\lambda (_: T).(\lambda (u4: T).(eq C c4 (CHead e2 (Flat f) u4)))))))
(\lambda (f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u3: T).(\lambda
-(_: T).(drop O O c3 (CHead e1 (Flat f) u3))))))) (\lambda (_: F).(\lambda (_:
-C).(\lambda (_: C).(\lambda (u3: T).(\lambda (u4: T).(subst0 O v0 u3 u4))))))
+(_: T).(drop i i c3 (CHead e1 (Flat f) u3))))))) (\lambda (_: F).(\lambda (_:
+C).(\lambda (_: C).(\lambda (u3: T).(\lambda (u4: T).(subst0 i v0 u3 u4))))))
(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda
-(_: T).(csubst0 O v0 e1 e2))))))))))).(\lambda (H5: (eq nat (S i) O)).(let H6
+(_: T).(csubst0 i v0 e1 e2))))))))))).(\lambda (H5: (eq nat (S i) O)).(let H6
\def (eq_ind nat (S i) (\lambda (ee: nat).(match ee in nat return (\lambda
(_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H5)
-in (False_ind (or4 (drop O O (CHead c3 (Bind b) u1) (CHead c4 (Bind b) u2))
-(ex3_4 F C T T (\lambda (f: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (u4:
-T).(eq C (CHead c4 (Bind b) u2) (CHead e0 (Flat f) u4)))))) (\lambda (f:
-F).(\lambda (e0: C).(\lambda (u3: T).(\lambda (_: T).(drop O O (CHead c3
-(Bind b) u1) (CHead e0 (Flat f) u3)))))) (\lambda (_: F).(\lambda (_:
-C).(\lambda (u3: T).(\lambda (u4: T).(subst0 O v0 u3 u4)))))) (ex3_4 F C C T
-(\lambda (f: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(eq C (CHead
-c4 (Bind b) u2) (CHead e2 (Flat f) u)))))) (\lambda (f: F).(\lambda (e1:
-C).(\lambda (_: C).(\lambda (u: T).(drop O O (CHead c3 (Bind b) u1) (CHead e1
-(Flat f) u)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda
-(_: T).(csubst0 O v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f: F).(\lambda
-(_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (u4: T).(eq C (CHead c4
-(Bind b) u2) (CHead e2 (Flat f) u4))))))) (\lambda (f: F).(\lambda (e1:
-C).(\lambda (_: C).(\lambda (u3: T).(\lambda (_: T).(drop O O (CHead c3 (Bind
-b) u1) (CHead e1 (Flat f) u3))))))) (\lambda (_: F).(\lambda (_: C).(\lambda
-(_: C).(\lambda (u3: T).(\lambda (u4: T).(subst0 O v0 u3 u4)))))) (\lambda
-(_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_:
-T).(csubst0 O v0 e1 e2)))))))) H6))))))))))))) (\lambda (f: F).(\lambda (i:
+in (False_ind (or4 (drop (S i) (S i) (CHead c3 (Bind b) u1) (CHead c4 (Bind
+b) u2)) (ex3_4 F C T T (\lambda (f: F).(\lambda (e0: C).(\lambda (_:
+T).(\lambda (u4: T).(eq C (CHead c4 (Bind b) u2) (CHead e0 (Flat f) u4))))))
+(\lambda (f: F).(\lambda (e0: C).(\lambda (u3: T).(\lambda (_: T).(drop (S i)
+(S i) (CHead c3 (Bind b) u1) (CHead e0 (Flat f) u3)))))) (\lambda (_:
+F).(\lambda (_: C).(\lambda (u3: T).(\lambda (u4: T).(subst0 (S i) v0 u3
+u4)))))) (ex3_4 F C C T (\lambda (f: F).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (u: T).(eq C (CHead c4 (Bind b) u2) (CHead e2 (Flat f) u))))))
+(\lambda (f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(drop (S i)
+(S i) (CHead c3 (Bind b) u1) (CHead e1 (Flat f) u)))))) (\lambda (_:
+F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 (S i) v0 e1
+e2)))))) (ex4_5 F C C T T (\lambda (f: F).(\lambda (_: C).(\lambda (e2:
+C).(\lambda (_: T).(\lambda (u4: T).(eq C (CHead c4 (Bind b) u2) (CHead e2
+(Flat f) u4))))))) (\lambda (f: F).(\lambda (e1: C).(\lambda (_: C).(\lambda
+(u3: T).(\lambda (_: T).(drop (S i) (S i) (CHead c3 (Bind b) u1) (CHead e1
+(Flat f) u3))))))) (\lambda (_: F).(\lambda (_: C).(\lambda (_: C).(\lambda
+(u3: T).(\lambda (u4: T).(subst0 (S i) v0 u3 u4)))))) (\lambda (_:
+F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0
+(S i) v0 e1 e2)))))))) H6))))))))))))) (\lambda (f: F).(\lambda (i:
nat).(\lambda (v0: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (H2: (subst0
i v0 u1 u2)).(\lambda (c3: C).(\lambda (c4: C).(\lambda (H3: (csubst0 i v0 c3
-c4)).(\lambda (H4: (((eq nat i O) \to (or4 (drop O O c3 c4) (ex3_4 F C T T
+c4)).(\lambda (H4: (((eq nat i O) \to (or4 (drop i i c3 c4) (ex3_4 F C T T
(\lambda (f0: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (u4: T).(eq C c4
(CHead e0 (Flat f0) u4)))))) (\lambda (f0: F).(\lambda (e0: C).(\lambda (u3:
-T).(\lambda (_: T).(drop O O c3 (CHead e0 (Flat f0) u3)))))) (\lambda (_:
-F).(\lambda (_: C).(\lambda (u3: T).(\lambda (u4: T).(subst0 O v0 u3 u4))))))
+T).(\lambda (_: T).(drop i i c3 (CHead e0 (Flat f0) u3)))))) (\lambda (_:
+F).(\lambda (_: C).(\lambda (u3: T).(\lambda (u4: T).(subst0 i v0 u3 u4))))))
(ex3_4 F C C T (\lambda (f0: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u:
T).(eq C c4 (CHead e2 (Flat f0) u)))))) (\lambda (f0: F).(\lambda (e1:
-C).(\lambda (_: C).(\lambda (u: T).(drop O O c3 (CHead e1 (Flat f0) u))))))
-(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 O
+C).(\lambda (_: C).(\lambda (u: T).(drop i i c3 (CHead e1 (Flat f0) u))))))
+(\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(csubst0 i
v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f0: F).(\lambda (_: C).(\lambda
(e2: C).(\lambda (_: T).(\lambda (u4: T).(eq C c4 (CHead e2 (Flat f0)
u4))))))) (\lambda (f0: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u3:
-T).(\lambda (_: T).(drop O O c3 (CHead e1 (Flat f0) u3))))))) (\lambda (_:
+T).(\lambda (_: T).(drop i i c3 (CHead e1 (Flat f0) u3))))))) (\lambda (_:
F).(\lambda (_: C).(\lambda (_: C).(\lambda (u3: T).(\lambda (u4: T).(subst0
-O v0 u3 u4)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda
-(_: T).(\lambda (_: T).(csubst0 O v0 e1 e2))))))))))).(\lambda (H5: (eq nat i
+i v0 u3 u4)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda
+(_: T).(\lambda (_: T).(csubst0 i v0 e1 e2))))))))))).(\lambda (H5: (eq nat i
O)).(let H6 \def (eq_ind nat i (\lambda (n0: nat).((eq nat n0 O) \to (or4
-(drop O O c3 c4) (ex3_4 F C T T (\lambda (f0: F).(\lambda (e0: C).(\lambda
+(drop n0 n0 c3 c4) (ex3_4 F C T T (\lambda (f0: F).(\lambda (e0: C).(\lambda
(_: T).(\lambda (u4: T).(eq C c4 (CHead e0 (Flat f0) u4)))))) (\lambda (f0:
-F).(\lambda (e0: C).(\lambda (u3: T).(\lambda (_: T).(drop O O c3 (CHead e0
+F).(\lambda (e0: C).(\lambda (u3: T).(\lambda (_: T).(drop n0 n0 c3 (CHead e0
(Flat f0) u3)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u3: T).(\lambda
-(u4: T).(subst0 O v0 u3 u4)))))) (ex3_4 F C C T (\lambda (f0: F).(\lambda (_:
-C).(\lambda (e2: C).(\lambda (u: T).(eq C c4 (CHead e2 (Flat f0) u))))))
-(\lambda (f0: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(drop O O
+(u4: T).(subst0 n0 v0 u3 u4)))))) (ex3_4 F C C T (\lambda (f0: F).(\lambda
+(_: C).(\lambda (e2: C).(\lambda (u: T).(eq C c4 (CHead e2 (Flat f0) u))))))
+(\lambda (f0: F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u: T).(drop n0 n0
c3 (CHead e1 (Flat f0) u)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2:
-C).(\lambda (_: T).(csubst0 O v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f0:
+C).(\lambda (_: T).(csubst0 n0 v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f0:
F).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (u4: T).(eq C c4
(CHead e2 (Flat f0) u4))))))) (\lambda (f0: F).(\lambda (e1: C).(\lambda (_:
-C).(\lambda (u3: T).(\lambda (_: T).(drop O O c3 (CHead e1 (Flat f0)
+C).(\lambda (u3: T).(\lambda (_: T).(drop n0 n0 c3 (CHead e1 (Flat f0)
u3))))))) (\lambda (_: F).(\lambda (_: C).(\lambda (_: C).(\lambda (u3:
-T).(\lambda (u4: T).(subst0 O v0 u3 u4)))))) (\lambda (_: F).(\lambda (e1:
-C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 O v0 e1
+T).(\lambda (u4: T).(subst0 n0 v0 u3 u4)))))) (\lambda (_: F).(\lambda (e1:
+C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0 n0 v0 e1
e2)))))))))) H4 O H5) in (let H7 \def (eq_ind nat i (\lambda (n0:
nat).(csubst0 n0 v0 c3 c4)) H3 O H5) in (let H8 \def (eq_ind nat i (\lambda
-(n0: nat).(subst0 n0 v0 u1 u2)) H2 O H5) in (or4_intro3 (drop O O (CHead c3
-(Flat f) u1) (CHead c4 (Flat f) u2)) (ex3_4 F C T T (\lambda (f0: F).(\lambda
-(e0: C).(\lambda (_: T).(\lambda (u4: T).(eq C (CHead c4 (Flat f) u2) (CHead
-e0 (Flat f0) u4)))))) (\lambda (f0: F).(\lambda (e0: C).(\lambda (u3:
-T).(\lambda (_: T).(drop O O (CHead c3 (Flat f) u1) (CHead e0 (Flat f0)
+(n0: nat).(subst0 n0 v0 u1 u2)) H2 O H5) in (eq_ind_r nat O (\lambda (n0:
+nat).(or4 (drop n0 n0 (CHead c3 (Flat f) u1) (CHead c4 (Flat f) u2)) (ex3_4 F
+C T T (\lambda (f0: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (u4: T).(eq
+C (CHead c4 (Flat f) u2) (CHead e0 (Flat f0) u4)))))) (\lambda (f0:
+F).(\lambda (e0: C).(\lambda (u3: T).(\lambda (_: T).(drop n0 n0 (CHead c3
+(Flat f) u1) (CHead e0 (Flat f0) u3)))))) (\lambda (_: F).(\lambda (_:
+C).(\lambda (u3: T).(\lambda (u4: T).(subst0 n0 v0 u3 u4)))))) (ex3_4 F C C T
+(\lambda (f0: F).(\lambda (_: C).(\lambda (e2: C).(\lambda (u: T).(eq C
+(CHead c4 (Flat f) u2) (CHead e2 (Flat f0) u)))))) (\lambda (f0: F).(\lambda
+(e1: C).(\lambda (_: C).(\lambda (u: T).(drop n0 n0 (CHead c3 (Flat f) u1)
+(CHead e1 (Flat f0) u)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2:
+C).(\lambda (_: T).(csubst0 n0 v0 e1 e2)))))) (ex4_5 F C C T T (\lambda (f0:
+F).(\lambda (_: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (u4: T).(eq C
+(CHead c4 (Flat f) u2) (CHead e2 (Flat f0) u4))))))) (\lambda (f0:
+F).(\lambda (e1: C).(\lambda (_: C).(\lambda (u3: T).(\lambda (_: T).(drop n0
+n0 (CHead c3 (Flat f) u1) (CHead e1 (Flat f0) u3))))))) (\lambda (_:
+F).(\lambda (_: C).(\lambda (_: C).(\lambda (u3: T).(\lambda (u4: T).(subst0
+n0 v0 u3 u4)))))) (\lambda (_: F).(\lambda (e1: C).(\lambda (e2: C).(\lambda
+(_: T).(\lambda (_: T).(csubst0 n0 v0 e1 e2))))))))) (or4_intro3 (drop O O
+(CHead c3 (Flat f) u1) (CHead c4 (Flat f) u2)) (ex3_4 F C T T (\lambda (f0:
+F).(\lambda (e0: C).(\lambda (_: T).(\lambda (u4: T).(eq C (CHead c4 (Flat f)
+u2) (CHead e0 (Flat f0) u4)))))) (\lambda (f0: F).(\lambda (e0: C).(\lambda
+(u3: T).(\lambda (_: T).(drop O O (CHead c3 (Flat f) u1) (CHead e0 (Flat f0)
u3)))))) (\lambda (_: F).(\lambda (_: C).(\lambda (u3: T).(\lambda (u4:
T).(subst0 O v0 u3 u4)))))) (ex3_4 F C C T (\lambda (f0: F).(\lambda (_:
C).(\lambda (e2: C).(\lambda (u: T).(eq C (CHead c4 (Flat f) u2) (CHead e2
C).(\lambda (u3: T).(\lambda (u4: T).(subst0 O v0 u3 u4)))))) (\lambda (_:
F).(\lambda (e1: C).(\lambda (e2: C).(\lambda (_: T).(\lambda (_: T).(csubst0
O v0 e1 e2)))))) f c3 c4 u1 u2 (refl_equal C (CHead c4 (Flat f) u2))
-(drop_refl (CHead c3 (Flat f) u1)) H8 H7)))))))))))))))) k)) y v c1 c2 H1)))
-H) e (drop_gen_refl c2 e H0)))))))) (\lambda (n0: nat).(\lambda (IHn:
+(drop_refl (CHead c3 (Flat f) u1)) H8 H7)) i H5))))))))))))))) k)) y v c1 c2
+H1))) H) e (drop_gen_refl c2 e H0)))))))) (\lambda (n0: nat).(\lambda (IHn:
((\forall (c1: C).(\forall (c2: C).(\forall (v: T).((csubst0 n0 v c1 c2) \to
(\forall (e: C).((drop n0 O c2 e) \to (or4 (drop n0 O c1 e) (ex3_4 F C T T
(\lambda (f: F).(\lambda (e0: C).(\lambda (_: T).(\lambda (u2: T).(eq C e