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