DEFINITION subst1_head()
TYPE =
       ∀v:T
         .∀u1:T
           .∀u2:T
             .∀i:nat
               .(subst1 i v u1 u2)→∀k:K.∀t1:T.∀t2:T.(subst1 (s k i) v t1 t2)→(subst1 i v (THead k u1 t1) (THead k u2 t2))
BODY =
Show proof