(* case 2.1 : i0 = 0 *)
DropGenBase; Inversion H2; Clear H2.
Rewrite <- H5; Rewrite H6 in H; Rewrite <- H7 in H3; Clear H5 H6 H7 d0 k u0.
(* case 2.1 : i0 = 0 *)
DropGenBase; Inversion H2; Clear H2.
Rewrite <- H5; Rewrite H6 in H; Rewrite <- H7 in H3; Clear H5 H6 H7 d0 k u0.