-c2)).(or3_ind (ex3_2 T nat (\lambda (_: T).(\lambda (j: nat).(eq nat (s k i)
-(s k j)))) (\lambda (u2: T).(\lambda (_: nat).(eq C c2 (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 i) (s k j)))) (\lambda (c3:
-C).(\lambda (_: nat).(eq C c2 (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 i) (s k j))))) (\lambda (u2: T).(\lambda
-(c3: C).(\lambda (_: nat).(eq C c2 (CHead c3 k u2))))) (\lambda (u2:
-T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1 u2)))) (\lambda (_:
-T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v c1 c3))))) (ex3_2 T C
-(\lambda (u2: T).(\lambda (c3: C).(eq C c2 (CHead c3 k u2)))) (\lambda (u2:
-T).(\lambda (_: C).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (c3:
-C).(csubst1 i v c1 c3)))) (\lambda (H1: (ex3_2 T nat (\lambda (_: T).(\lambda
-(j: nat).(eq nat (s k i) (s k j)))) (\lambda (u2: T).(\lambda (_: nat).(eq C
-c2 (CHead c1 k u2)))) (\lambda (u2: T).(\lambda (j: nat).(subst0 j v u1
-u2))))).(ex3_2_ind T nat (\lambda (_: T).(\lambda (j: nat).(eq nat (s k i) (s
-k j)))) (\lambda (u2: T).(\lambda (_: nat).(eq C c2 (CHead c1 k u2))))
-(\lambda (u2: T).(\lambda (j: nat).(subst0 j v u1 u2))) (ex3_2 T C (\lambda
-(u2: T).(\lambda (c3: C).(eq C c2 (CHead c3 k u2)))) (\lambda (u2:
-T).(\lambda (_: C).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (c3:
-C).(csubst1 i v c1 c3)))) (\lambda (x0: T).(\lambda (x1: nat).(\lambda (H2:
-(eq nat (s k i) (s k x1))).(\lambda (H3: (eq C c2 (CHead c1 k x0))).(\lambda
-(H4: (subst0 x1 v u1 x0)).(eq_ind_r C (CHead c1 k x0) (\lambda (c: C).(ex3_2
-T C (\lambda (u2: T).(\lambda (c3: C).(eq C c (CHead c3 k u2)))) (\lambda
-(u2: T).(\lambda (_: C).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (c3:
-C).(csubst1 i v c1 c3))))) (let H5 \def (eq_ind_r nat x1 (\lambda (n:
-nat).(subst0 n v u1 x0)) H4 i (s_inj k i x1 H2)) in (ex3_2_intro T C (\lambda
+c2)).(let H1 \def (csubst0_gen_head k c1 c2 u1 v (s k i) H0) in (or3_ind
+(ex3_2 T nat (\lambda (_: T).(\lambda (j: nat).(eq nat (s k i) (s k j))))
+(\lambda (u2: T).(\lambda (_: nat).(eq C c2 (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 i) (s k j)))) (\lambda (c3: C).(\lambda (_:
+nat).(eq C c2 (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 i) (s k j))))) (\lambda (u2: T).(\lambda (c3: C).(\lambda
+(_: nat).(eq C c2 (CHead c3 k u2))))) (\lambda (u2: T).(\lambda (_:
+C).(\lambda (j: nat).(subst0 j v u1 u2)))) (\lambda (_: T).(\lambda (c3:
+C).(\lambda (j: nat).(csubst0 j v c1 c3))))) (ex3_2 T C (\lambda (u2:
+T).(\lambda (c3: C).(eq C c2 (CHead c3 k u2)))) (\lambda (u2: T).(\lambda (_:
+C).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (c3: C).(csubst1 i v c1
+c3)))) (\lambda (H2: (ex3_2 T nat (\lambda (_: T).(\lambda (j: nat).(eq nat
+(s k i) (s k j)))) (\lambda (u2: T).(\lambda (_: nat).(eq C c2 (CHead c1 k
+u2)))) (\lambda (u2: T).(\lambda (j: nat).(subst0 j v u1 u2))))).(ex3_2_ind T
+nat (\lambda (_: T).(\lambda (j: nat).(eq nat (s k i) (s k j)))) (\lambda
+(u2: T).(\lambda (_: nat).(eq C c2 (CHead c1 k u2)))) (\lambda (u2:
+T).(\lambda (j: nat).(subst0 j v u1 u2))) (ex3_2 T C (\lambda (u2:
+T).(\lambda (c3: C).(eq C c2 (CHead c3 k u2)))) (\lambda (u2: T).(\lambda (_:
+C).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (c3: C).(csubst1 i v c1
+c3)))) (\lambda (x0: T).(\lambda (x1: nat).(\lambda (H3: (eq nat (s k i) (s k
+x1))).(\lambda (H4: (eq C c2 (CHead c1 k x0))).(\lambda (H5: (subst0 x1 v u1
+x0)).(eq_ind_r C (CHead c1 k x0) (\lambda (c: C).(ex3_2 T C (\lambda (u2:
+T).(\lambda (c3: C).(eq C c (CHead c3 k u2)))) (\lambda (u2: T).(\lambda (_:
+C).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (c3: C).(csubst1 i v c1
+c3))))) (let H_y \def (s_inj k i x1 H3) in (let H6 \def (eq_ind_r nat x1
+(\lambda (n: nat).(subst0 n v u1 x0)) H5 i H_y) in (ex3_2_intro T C (\lambda