DEFINITION csubst1_gen_head()
TYPE =
       ∀k:K
         .∀c1:C
           .∀x:C
             .∀u1:T
               .∀v:T
                 .∀i:nat
                   .csubst1 (s k i) v (CHead c1 k u1) x
                     →ex3_2 T C λu2:T.λc2:C.eq C x (CHead c2 k u2) λu2:T.λ:C.subst1 i v u1 u2 λ:T.λc2:C.csubst1 i v c1 c2
BODY =
Show proof