+(_: 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