X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fcsubst0%2Fdrop.ma;h=814c2eb1e48d38d8e56e2f493af7c41c8494e29c;hb=6329f0f87906d3347c39d2ba2f5ec2b2124f17a2;hp=b1a0632080a04ebd721314473382ee79ab11168a;hpb=831af787465e1bff886e22ee14b68c8f1bb0177c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/drop.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/drop.ma
index b1a063208..814c2eb1e 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/drop.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/drop.ma
@@ -2564,347 +2564,406 @@ 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))))))))) (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: 
@@ -2928,8 +2987,8 @@ u1) (CHead e1 (Flat f0) u))))))) (\lambda (f0: 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)))))) 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 
@@ -4775,84 +4834,104 @@ 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))))))))) (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 
@@ -4874,252 +4953,292 @@ 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 (_: 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 
@@ -5141,8 +5260,8 @@ u2) (CHead e2 (Flat f0) u4))))))) (\lambda (f0: F).(\lambda (e1: 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)))))) 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