Monoidal categories: coherence from strictness

The proof should go as follows.

In the strict monoidal category, we have that the corresponding compositions of $\alpha'$, $\alpha^{\prime -1}$, $l'$, $l^{\prime-1}$, $r'$, $r^{\prime -1}$ are all the identity.

Let $P_{Fi}$ be the corresponding parenthesization of $FX_1,\ldots,FX_n$ and $1'$s to $P_i$. Monoidality of the equivalence gives natural isomorphisms $\alpha_i : FP_i \to P_{Fi}$ such that $$ \require{AMScd} \begin{CD} FP_1 @>F f>> FP_2\\ @V\alpha_1 VV @V\alpha_2 VV \\ P_{F1} @> \mathrm{id} >> P_{F2}. \end{CD} $$ The same diagram commutes for $g$, so $Ff=Fg$. Then by faithfulness of $F$, $f=g$.

Constructing $\alpha_i$

It sounds like you're having trouble with constructing the $\alpha_i$, so I'll expand on this a bit. This goes inductively, so we just need to deal with the outermost layer of $P_1$ or $P_2$. We'll just look at $P_1$.

If $P_1 = X\otimes Y$, then $FP_1 = F(X\otimes Y)$ and $P_{F1} = X_F \otimes Y_F$, where the $F$ subscript refers to the appropriate product of $F$ applied to the atoms. Then we have the monoidal structure isomorphism $J : F(X\otimes Y) \to F(X)\otimes F(Y)$, and then we inductively construct $\alpha_X : F(X)\to X_F$ and $\alpha_Y : F(Y)\to Y_F$. The composite $(\alpha_X \otimes \alpha_Y) \circ J$ gives the desired isomorphism $FP_1\to P_{F1}$.

On the other hand, if $P_1 = I\otimes X$, then $P_{F1} = I'\otimes X_F$. This time, if $\iota : F(I)\to I'$ is the natural isomorphism, we take the composite $$F(I\otimes X)\overset{J}{\to} F(I)\otimes FX \overset{\iota\otimes \alpha_X}{\to} I'\otimes X_F= P_{F1}$$

For $P_1 = X\otimes I$ we do the same thing but modified for symmetry.

Hopefully this helps. I can expand on this if needed.

Edit, an expansion on why the diagram commutes.

This is also proved inductively.

Suppose the outermost function in $f$ is an associator, which I'll denote by $a$ and $a'$ in the two categories in the equivalence in $C_s$, $a'=\mathrm{id}$, since I used $\alpha$ for the natural isomorphisms.

Then $f=a\circ f_0$ and $f'=a'\circ f_0'$, with $f:P_1\to P_2$ and $P_2 : X\otimes (Y \otimes Z$ for some products $X$, $Y$, and $Z$, so $f_0 : P_1\to (X\otimes Y)\otimes Z$. Then we have the commutative diagram $$ \newcommand\id{\mathrm{id}} \begin{CD} FP_1 @>f_0>> F((X\otimes Y) \otimes Z) @>Fa>> F(X \otimes (Y\otimes Z)) \\ @VVV @VJVV @VJVV \\ @. F(X\otimes Y) \otimes FZ @. FX\otimes F(Y\otimes Z) \\ @V\alpha_1 VV @VJ\otimes \id VV @V\id \otimes J VV \\ @. (FX\otimes FY)\otimes FZ @>a'>> FX\otimes (FY\otimes FZ)\\ @VVV @V(\alpha_X\otimes \alpha_Y)\otimes \alpha_Z VV @V\alpha_X \otimes (\alpha_Y\otimes \alpha_Z)VV \\ P_{F1} @>f'_0>> (X_F\otimes Y_F)\otimes Z_F @>a'>> X_F \otimes (Y_F\otimes Z_F) \\ \end{CD} $$ The left rectangle commutes by the inductive hypothesis applied to $f_0$, since the middle vertical composite is the definition of the $\alpha$ map for $(X\otimes Y)\otimes Z$. The top right rectangle commutes by the compatibility condition for $J$. The bottom right square commutes by naturality of the associator. By symmetry, the same argument applies to $a^{-1}$.

Now we need to do the same thing for the left and right units and their inverses. By symmetry, it suffices to prove commutativity when the outermost map in $f$ is $l$.

Then $f = l\circ f_0$, with $f_0 : P_1\to I\otimes P_2$. This time, we get the diagram $$ \begin{CD} FP_1 @>f_0>> F(I\otimes P_2) @>Fl>> FP_2 \\ @VVV @VJVV @V\id VV \\ @. FI\otimes FP_2 @. FP_2 \\ @V\alpha_1 VV @V \iota \otimes \id VV @V\id VV \\ @. I'\otimes FP_2 @>l'>> FP_2 \\ @VVV @V\id \otimes \alpha_2 VV @V\alpha_2VV \\ P_{F1} @>f'_0>> I'\otimes P_{F2} @>l'>> P_{F2} \\ \end{CD} $$ Again, the left rectangle commutes by the inductive hypothesis, the top right rectangle is the coherence condition for $\iota$, and the bottom right square is naturality of $l'$.

This completes the proof.