Structural Induction

I'm strugling with an structural induction with the following rules:

count' acc [] = acc

count' acc(x:xs) = count' (1+acc)xs



[] + ys = ys

(x:xs)++ys = x:(xs++ys)



and I have to prove:

count'(count'acc ys) xs = count' acc (ys ++ xs)



I did the base case, and the for the step case:



count'(count' acc as)xs = count' acc (as ++ xs) - IH (induction hypothesis)



so for all a in as this should work, so I rewrote it as:



count'(count' acc (a:as))xs = count'acc (a:as ++ xs)



then I tried go get from one side to the other, but I couldnt. I got stuck at

count'(count' (1+acc)as)xs.

If it wasn't for that "1+" I'd be able to do that, but now I don't know how to proceed... please help!