(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.
-(* case 1 : subst0_bref *)
+(* case 1 : subst0_lref *)
Arith5 i0 i; XEAuto.
(* case 2 : subst0_fst *)
IH; XEAuto.
(u1,u:?; i:?) (subst0 i u u2 u1) ->
(EX t | (subst0 j u1 t1 t) & (subst0 (S (plus i j)) u t2 t)).
Intros until 1; XElim H; Intros.
-(* case 1 : subst0_bref *)
+(* case 1 : subst0_lref *)
Arith5 i0 i; XEAuto.
(* case 2 : subst0_fst *)
IH; XEAuto.