How to use structural induction to prove law on lists

Question

I want to prove that the following equation holds using structural induction on (finite) lists

subs (map f xs) = map (map f) (subs xs)

where subs [] = [[]]                                          (subs.1)
      subs (x:xs) = subs (xs) ++ map (x:) (subs xs)           (subs.2)

      map f [] = []                                           (map.1)
      map f (x:xs) = f x : map f xs                           (map.2)

: is the cons operator and ++ the join operator on lists.

I'm using structural induction on xs, the base step for [] is easy to prove but I hit a wall when trying to solve the inductive step for (x:xs)

subs (map f) (x:xs)                                             (map.2)
subs (f x : map f xs)                                           (subs.2)
subs (map f xs) ++ map ((f x):) (subs (map f xs))               (hyp)
(map (map f) (subs xs)) ++ map ((f x):) (map (map f)(subs xs)) 

From here I couldn't find a way to proceed so I moved to the right-hand side of the equation and I kind of found a way to find a "proof" but something tells me that it's bogus

map (map f) (subs (x:xs))                     (subs.2)
map (map f) (subs xs ++ map (x:) (subs xs))   (generalise term)
map (map f) ys                                (hyp)
subs (map f ys)                               ???
subs (map f (y:ys)) 
□

My reasoning here is: (x:xs) is a list with at least length 1, it should be legal to generalise subs xs ++ map (x:) (subs xs) as either (y:ys) or ys (because (x:xs) is not empty) so I chose the latter first to be able to use the induction hypothesis and after that I rewritten ys as (y:ys) to establish the case.

Does this make any sense at all? If not, could anybody show me the right approach to tackle this proof?