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