How to use structural induction to prove law on lists
You'll want a helper lemma to make this endeavor more digestible.



Notations for map and subs:

I'm going to condense the map notation a bit so that we can express it as the binary operator $f \diamond l = \mathrm{map} ~ f ~ l$. Similarly, we will express the subs as a unary operation $\lfloor\!\!\lfloor l \rfloor\!\!\rfloor = \mathrm{subs} ~ l$.

This might seem terse at the moment, but it's useful to visually capture a "commutativity" property we will illustrate in a moment that sits at the core of the proof of this extensional equation.

Reformulation of the problem:

We want to show that
$$
\lfloor\!\!\lfloor f \diamond l \rfloor\!\!\rfloor = (f \diamond) \diamond \lfloor\!\!\lfloor l \rfloor\!\!\rfloor
$$

which basically states that if we try to hoist the $f$ outside of the brackets, then we have to turn it into a map.

Now, if we follow your original blueprint, your inductive hypothesis establishes that
$$
\lfloor\!\!\lfloor f \diamond x ::l \rfloor\!\!\rfloor = (f \diamond) \diamond \lfloor\!\!\lfloor l \rfloor\!\!\rfloor +\!\!\!+ ~(f ~x ::) \diamond ((f \diamond) \diamond \lfloor\!\!\lfloor l \rfloor\!\!\rfloor)
$$

In order for this proof to proceed, you need to tame the term on the righthand side of the concatenation. But what would you want it to look like?

Well, recall that maps distribute into concatenations:
$$
(f \diamond l_1) +\!\!\!+ ~(f \diamond l_2) = f \diamond (l_1 +\!\!\!+~ l_2)
$$

which suggests that we might be able to get our equation into an amenable form if we can rewrite the second term so that it is of the form $(f \diamond) \diamond \cdot$.

Here's where our helper lemma comes in to save the day:

Lemma ("Commutativity"):You have to use finger quotes when you read the name of this lemma out loud.
$$
(f ~x ::) \diamond ((f \diamond) \diamond l) = (f \diamond) \diamond ((x ::) \diamond l)
$$
Proof: Structural induction on $l$. This is actually a pretty easy proof, so I'll leave it to the reader™. However, the core of this proof is essentially showing that
\begin{align*}
(f~x ::) \diamond ((f \diamond) \diamond a :: [...]) &amp;= (f~x ::) \diamond ((f \diamond a) :: \underbrace{((f \diamond) \diamond [...])}_{\text{induction hypothesis}}) \\
&amp;= \underbrace{(f~x :: f \diamond a)}_{\text{map distributivity}} :: (f~x ::) \diamond((f \diamond) \diamond [...])) \\
&amp;= (f \diamond (x :: a)) :: (f~x ::) \diamond((f \diamond) \diamond [...])) \\
&amp; \text{discharge the induction hypothesis} \\
&amp;= (f \diamond (x :: a)) :: (f \diamond) \diamond ((x ::) \diamond [...]) \\
&amp; \text{distributivity} \\
&amp;= (f \diamond) \diamond ((x :: a) :: ((x ::) \diamond [...])) \\
&amp; \text{distributivity} \\
&amp;= (f \diamond) \diamond ((x ::) \diamond (a :: [...]))
\end{align*}
which concludes the proof of the lemma. $\square$

Finishing your inductive proof:

Once we have this gem, we can continue your structural induction proof.

\begin{align*}
\lfloor\!\!\lfloor f \diamond x ::l \rfloor\!\!\rfloor &amp;= (f \diamond) \diamond \lfloor\!\!\lfloor l \rfloor\!\!\rfloor +\!\!\!+ ~(f ~x ::) \diamond ((f \diamond) \diamond \lfloor\!\!\lfloor l \rfloor\!\!\rfloor) \\
&amp; \text{by the lemma} \\
&amp;= (f \diamond) \diamond \lfloor\!\!\lfloor l \rfloor\!\!\rfloor +\!\!\!+ ~(f\diamond) \diamond ((x ::) \diamond \lfloor\!\!\lfloor l \rfloor\!\!\rfloor) \\
&amp; \text{by distributivity of map} \\
&amp;= (f \diamond) \diamond (\lfloor\!\!\lfloor l \rfloor\!\!\rfloor +\!\!\!+ ~ (x::) \diamond \lfloor\!\!\lfloor l \rfloor\!\!\rfloor) \\
&amp; \text{by the definiton of } \lfloor\!\!\lfloor x :: l \rfloor\!\!\rfloor \\
&amp;= (f \diamond) \diamond \lfloor\!\!\lfloor x :: l \rfloor\!\!\rfloor
\end{align*}

which satisfies your goal.



The equational acrobatics we've just performed seems a bit excessive, which is why I'm willing to bet that there's some elegant fusion law, recursion scheme, or some other representation (probably some categorical law given the nature of the problem) that nicely unwraps this proof. Unfortunately, AFAIK, I'm not aware of more elegant approaches. While this is a valid proof, it's somewhat unsatisfying. It is as much of a proof of this theorem as my performances of Taylor Swift is considered entertainment: it is technically correct, just not in the way that I intend it to be.