-(c3: C).(\lambda (_: nat).(eq C x (CHead c3 k u2))))) (\lambda (u2:
-T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1 u2)))) (\lambda (_:
-T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1 c3))))))))))) (\lambda
-(H10: (eq K k0 k)).(eq_ind K k (\lambda (k1: K).((eq T u u1) \to ((eq C
-(CHead c2 k1 u) x) \to ((csubst0 i0 v c1 c2) \to (or3 (ex3_2 T nat (\lambda
-(_: T).(\lambda (j: nat).(eq nat (s k1 i0) (s k j)))) (\lambda (u2:
-T).(\lambda (_: nat).(eq C x (CHead c1 k u2)))) (\lambda (u2: T).(\lambda (j:
-nat).(subst0 j v u1 u2)))) (ex3_2 C nat (\lambda (_: C).(\lambda (j: nat).(eq
-nat (s k1 i0) (s k j)))) (\lambda (c3: C).(\lambda (_: nat).(eq C x (CHead c3
-k u1)))) (\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1 c3)))) (ex4_3 T C
-nat (\lambda (_: T).(\lambda (_: C).(\lambda (j: nat).(eq nat (s k1 i0) (s k
-j))))) (\lambda (u2: T).(\lambda (c3: C).(\lambda (_: nat).(eq C x (CHead c3
-k u2))))) (\lambda (u2: T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1
-u2)))) (\lambda (_: T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1
-c3)))))))))) (\lambda (H11: (eq T u u1)).(eq_ind T u1 (\lambda (t: T).((eq C
-(CHead c2 k t) x) \to ((csubst0 i0 v c1 c2) \to (or3 (ex3_2 T nat (\lambda
-(_: T).(\lambda (j: nat).(eq nat (s k i0) (s k j)))) (\lambda (u2:
-T).(\lambda (_: nat).(eq C x (CHead c1 k u2)))) (\lambda (u2: T).(\lambda (j:
-nat).(subst0 j v u1 u2)))) (ex3_2 C nat (\lambda (_: C).(\lambda (j: nat).(eq
-nat (s k i0) (s k j)))) (\lambda (c3: C).(\lambda (_: nat).(eq C x (CHead c3
-k u1)))) (\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1 c3)))) (ex4_3 T C
-nat (\lambda (_: T).(\lambda (_: C).(\lambda (j: nat).(eq nat (s k i0) (s k
-j))))) (\lambda (u2: T).(\lambda (c3: C).(\lambda (_: nat).(eq C x (CHead c3
-k u2))))) (\lambda (u2: T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1
-u2)))) (\lambda (_: T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1
-c3))))))))) (\lambda (H12: (eq C (CHead c2 k u1) x)).(eq_ind C (CHead c2 k
-u1) (\lambda (c: C).((csubst0 i0 v c1 c2) \to (or3 (ex3_2 T nat (\lambda (_:
-T).(\lambda (j: nat).(eq nat (s k i0) (s k j)))) (\lambda (u2: T).(\lambda
-(_: nat).(eq C c (CHead c1 k u2)))) (\lambda (u2: T).(\lambda (j:
-nat).(subst0 j v u1 u2)))) (ex3_2 C nat (\lambda (_: C).(\lambda (j: nat).(eq
-nat (s k i0) (s k j)))) (\lambda (c3: C).(\lambda (_: nat).(eq C c (CHead c3
-k u1)))) (\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1 c3)))) (ex4_3 T C
-nat (\lambda (_: T).(\lambda (_: C).(\lambda (j: nat).(eq nat (s k i0) (s k
-j))))) (\lambda (u2: T).(\lambda (c3: C).(\lambda (_: nat).(eq C c (CHead c3
-k u2))))) (\lambda (u2: T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1
-u2)))) (\lambda (_: T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1
-c3)))))))) (\lambda (H13: (csubst0 i0 v c1 c2)).(let H14 \def (eq_ind K k0
-(\lambda (k1: K).(eq nat (s k1 i0) i)) H1 k H10) in (or3_intro1 (ex3_2 T nat
-(\lambda (_: T).(\lambda (j: nat).(eq nat (s k i0) (s k j)))) (\lambda (u2:
-T).(\lambda (_: nat).(eq C (CHead c2 k u1) (CHead c1 k u2)))) (\lambda (u2:
-T).(\lambda (j: nat).(subst0 j v u1 u2)))) (ex3_2 C nat (\lambda (_:
-C).(\lambda (j: nat).(eq nat (s k i0) (s k j)))) (\lambda (c3: C).(\lambda
-(_: nat).(eq C (CHead c2 k u1) (CHead c3 k u1)))) (\lambda (c3: C).(\lambda
-(j: nat).(csubst0 j v c1 c3)))) (ex4_3 T C nat (\lambda (_: T).(\lambda (_:
-C).(\lambda (j: nat).(eq nat (s k i0) (s k j))))) (\lambda (u2: T).(\lambda
-(c3: C).(\lambda (_: nat).(eq C (CHead c2 k u1) (CHead c3 k u2))))) (\lambda
-(u2: T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1 u2)))) (\lambda (_:
-T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1 c3))))) (ex3_2_intro C
-nat (\lambda (_: C).(\lambda (j: nat).(eq nat (s k i0) (s k j)))) (\lambda
-(c3: C).(\lambda (_: nat).(eq C (CHead c2 k u1) (CHead c3 k u1)))) (\lambda
-(c3: C).(\lambda (j: nat).(csubst0 j v c1 c3))) c2 i0 (refl_equal nat (s k
-i0)) (refl_equal C (CHead c2 k u1)) H13)))) x H12)) u (sym_eq T u u1 H11)))
-k0 (sym_eq K k0 k H10))) c0 (sym_eq C c0 c1 H9))) H8)) H7))) v0 (sym_eq T v0
-v H5))) i H1 H2 H3 H4 H0))))) | (csubst0_both k0 i0 v0 u0 u2 H0 c0 c2 H1)
-\Rightarrow (\lambda (H2: (eq nat (s k0 i0) i)).(\lambda (H3: (eq T v0
-v)).(\lambda (H4: (eq C (CHead c0 k0 u0) (CHead c1 k u1))).(\lambda (H5: (eq
-C (CHead c2 k0 u2) x)).(eq_ind nat (s k0 i0) (\lambda (n: nat).((eq T v0 v)
-\to ((eq C (CHead c0 k0 u0) (CHead c1 k u1)) \to ((eq C (CHead c2 k0 u2) x)
-\to ((subst0 i0 v0 u0 u2) \to ((csubst0 i0 v0 c0 c2) \to (or3 (ex3_2 T nat
-(\lambda (_: T).(\lambda (j: nat).(eq nat n (s k j)))) (\lambda (u3:
-T).(\lambda (_: nat).(eq C x (CHead c1 k u3)))) (\lambda (u3: T).(\lambda (j:
-nat).(subst0 j v u1 u3)))) (ex3_2 C nat (\lambda (_: C).(\lambda (j: nat).(eq
-nat n (s k j)))) (\lambda (c3: C).(\lambda (_: nat).(eq C x (CHead c3 k
-u1)))) (\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1 c3)))) (ex4_3 T C
-nat (\lambda (_: T).(\lambda (_: C).(\lambda (j: nat).(eq nat n (s k j)))))
-(\lambda (u3: T).(\lambda (c3: C).(\lambda (_: nat).(eq C x (CHead c3 k
-u3))))) (\lambda (u3: T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1
-u3)))) (\lambda (_: T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1
-c3)))))))))))) (\lambda (H6: (eq T v0 v)).(eq_ind T v (\lambda (t: T).((eq C
-(CHead c0 k0 u0) (CHead c1 k u1)) \to ((eq C (CHead c2 k0 u2) x) \to ((subst0
-i0 t u0 u2) \to ((csubst0 i0 t c0 c2) \to (or3 (ex3_2 T nat (\lambda (_:
-T).(\lambda (j: nat).(eq nat (s k0 i0) (s k j)))) (\lambda (u3: T).(\lambda
-(_: nat).(eq C x (CHead c1 k u3)))) (\lambda (u3: T).(\lambda (j:
-nat).(subst0 j v u1 u3)))) (ex3_2 C nat (\lambda (_: C).(\lambda (j: nat).(eq
-nat (s k0 i0) (s k j)))) (\lambda (c3: C).(\lambda (_: nat).(eq C x (CHead c3
-k u1)))) (\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1 c3)))) (ex4_3 T C
-nat (\lambda (_: T).(\lambda (_: C).(\lambda (j: nat).(eq nat (s k0 i0) (s k
-j))))) (\lambda (u3: T).(\lambda (c3: C).(\lambda (_: nat).(eq C x (CHead c3
-k u3))))) (\lambda (u3: T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1
-u3)))) (\lambda (_: T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1
-c3))))))))))) (\lambda (H7: (eq C (CHead c0 k0 u0) (CHead c1 k u1))).(let H8
-\def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T)
-with [(CSort _) \Rightarrow u0 | (CHead _ _ t) \Rightarrow t])) (CHead c0 k0
-u0) (CHead c1 k u1) H7) in ((let H9 \def (f_equal C K (\lambda (e: C).(match
-e in C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k0 | (CHead _ k1
-_) \Rightarrow k1])) (CHead c0 k0 u0) (CHead c1 k u1) H7) in ((let H10 \def
-(f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with
-[(CSort _) \Rightarrow c0 | (CHead c _ _) \Rightarrow c])) (CHead c0 k0 u0)
-(CHead c1 k u1) H7) in (eq_ind C c1 (\lambda (c: C).((eq K k0 k) \to ((eq T
-u0 u1) \to ((eq C (CHead c2 k0 u2) x) \to ((subst0 i0 v u0 u2) \to ((csubst0
-i0 v c c2) \to (or3 (ex3_2 T nat (\lambda (_: T).(\lambda (j: nat).(eq nat (s
-k0 i0) (s k j)))) (\lambda (u3: T).(\lambda (_: nat).(eq C x (CHead c1 k
-u3)))) (\lambda (u3: T).(\lambda (j: nat).(subst0 j v u1 u3)))) (ex3_2 C nat
-(\lambda (_: C).(\lambda (j: nat).(eq nat (s k0 i0) (s k j)))) (\lambda (c3:
-C).(\lambda (_: nat).(eq C x (CHead c3 k u1)))) (\lambda (c3: C).(\lambda (j:
-nat).(csubst0 j v c1 c3)))) (ex4_3 T C nat (\lambda (_: T).(\lambda (_:
-C).(\lambda (j: nat).(eq nat (s k0 i0) (s k j))))) (\lambda (u3: T).(\lambda
-(c3: C).(\lambda (_: nat).(eq C x (CHead c3 k u3))))) (\lambda (u3:
-T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1 u3)))) (\lambda (_:
-T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1 c3)))))))))))) (\lambda
-(H11: (eq K k0 k)).(eq_ind K k (\lambda (k1: K).((eq T u0 u1) \to ((eq C
-(CHead c2 k1 u2) x) \to ((subst0 i0 v u0 u2) \to ((csubst0 i0 v c1 c2) \to
-(or3 (ex3_2 T nat (\lambda (_: T).(\lambda (j: nat).(eq nat (s k1 i0) (s k
-j)))) (\lambda (u3: T).(\lambda (_: nat).(eq C x (CHead c1 k u3)))) (\lambda
-(u3: T).(\lambda (j: nat).(subst0 j v u1 u3)))) (ex3_2 C nat (\lambda (_: