Developing invariants for comparing two strings
I would not simplify $(2)$ at all. Just apply the rules for if, =, and command composition. Use weakening (pre- or post- rules) when convenient to do so.

Below, I added an empty else branch for clarity.

// (2): (S1 = S2 &lt;=&gt; X = Y \land E = true) 
//            \land \lnot(X != /\ \land Y != /\ \land E = true)
if !(X == /\ and Y == /\)
  // (3a): (2) \land (X != /\ \lor Y != /\)
  // (3b): S1 != S2 \land false = false
  E = false 
  // (3): S1 != S2 \land E = false
  // (4): S1 = S2 &lt;=&gt; E = true
else
  // (3c): (2) \land X = /\ \land Y = /\
  // (4): S1 = S2 &lt;=&gt; E = true
// (4): S1 = S2 &lt;=&gt; E = true
return E


Above, we used weakening, so we are left with proving:


$3a\implies 3b$. By contradiction, assume $\lnot 3b:\ S_1=S_2$ and $3a$. Since $S_1=S_2$, then by $2$ (part of $3a$) we have that $X=Y \land E=true$. We also know that at least one of $X,Y$ is not empty from $3a$, hence both are not empty since they are equal. This contradicts the last part of $2$, namely $\lnot(X\neq\Lambda \land Y\neq\Lambda \land E=true)$.
$3 \implies 4$. Two truths are always equivalent.
$3c \implies 4$. Replacing both $X,Y$ in $2$ with $\Lambda$, the first part of property $2$ immediately simplifies into $4$.


The first item can also be proved more formally, but I think you get the idea.



About your attempt: you used the equivalence

$$
\begin{array}{l}
\big((S_1 = S_2 \iff X = Y \land E = true) \land (X = \Lambda)\big) 
\\
\equiv (S_1 = S_2 \iff X = \Lambda \land Y = \Lambda \land E = true)
\end{array}
$$

However, this does not hold in general, e.g. for $X={\sf x}, Y={\sf y}, S_1=\Lambda, S_2={\sf h}, E=true$. Or, more in general, when $X$ is non empty, and $S_1\neq S_2$. In such case, the former is false, but the latter is true.