DEFINITION csubst0_gen_head()
TYPE =
       ∀k:K
         .∀c1:C
           .∀x:C
             .∀u1:T
               .∀v:T
                 .∀i:nat
                   .csubst0 i v (CHead c1 k u1) x
                     →(or3
                          ex3_2
                            T
                            nat
                            λ:T.λj:nat.eq nat i (s k j)
                            λu2:T.λ:nat.eq C x (CHead c1 k u2)
                            λu2:T.λj:nat.subst0 j v u1 u2
                          ex3_2
                            C
                            nat
                            λ:C.λj:nat.eq nat i (s k j)
                            λc2:C.λ:nat.eq C x (CHead c2 k u1)
                            λc2:C.λj:nat.csubst0 j v c1 c2
                          ex4_3
                            T
                            C
                            nat
                            λ:T.λ:C.λj:nat.eq nat i (s k j)
                            λu2:T.λc2:C.λ:nat.eq C x (CHead c2 k u2)
                            λu2:T.λ:C.λj:nat.subst0 j v u1 u2
                            λ:T.λc2:C.λj:nat.csubst0 j v c1 c2)
BODY =
Show proof