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