(u1,u:?; i:?) (subst0 i u u1 u2) ->
(EX t | (subst0 j u1 t1 t) & (subst0 (S (plus i j)) u t t2)).
Intros until 1; XElim H; Intros.
(u1,u:?; i:?) (subst0 i u u1 u2) ->
(EX t | (subst0 j u1 t1 t) & (subst0 (S (plus i j)) u t t2)).
Intros until 1; XElim H; Intros.