(subst (s k i) v0 t3) H3) (subst i v0 u1) H1) (subst i v0 (THead k u2 t4))
(subst_head k v0 u2 t4 i)) (subst i v0 (THead k u1 t3)) (subst_head k v0 u1
t3 i))))))))))))) d v t1 t2 H))))).
(subst (s k i) v0 t3) H3) (subst i v0 u1) H1) (subst i v0 (THead k u2 t4))
(subst_head k v0 u2 t4 i)) (subst i v0 (THead k u1 t3)) (subst_head k v0 u1
t3 i))))))))))))) d v t1 t2 H))))).