Equivalence rules for LTL - Getting stuck working with $ \square \lozenge $ & Until ($\textsf{ U}$ ) operators

Need to prove equivalence for (or disprove equivalence for):

$
\hspace{1cm}\square ϕ → \lozenge ψ ≡ ϕ\textsf{ U }(ψ ∨ ¬ϕ) \\
$

My current attempt using the LTL equivalnce rules to determine equivalence:

$
\square ϕ → \lozenge ψ \\
≡\
¬\square ϕ \lor \lozenge ψ \hspace{1cm}(\textsf{"Mutual implication"} ϕ →ψ≡¬ϕ\lor ψ )\\
≡
\lozenge ¬ϕ \lor \lozenge ψ \hspace{1cm}(\textsf{"Duality"} ¬\square≡\lozenge ¬ )\\
≡
\lozenge (¬ϕ \lor ψ) \hspace{1cm}(\textsf{"Distributive law on"}\lozenge )\\
≡true \textsf{ U} (¬ϕ \lor ψ) \hspace{1cm}(\textsf{"Def of"}\lozenge )\\
≡true \textsf{ U} (ψ \lor ¬ϕ) \hspace{1cm}(\textsf{"Symmetry"}\lor)\\
$

After this I got stuck. I am not sure how to proceed from here to get the right side. Are other propositional logic rules allowed to be used in LTL, like for example identity disjunction?

In order to prove the equivalence of two formulas $\phi,\psi$, it is enough to show that for every computation $\pi$, it holds that $\pi\models \phi$ iff $\pi\models \psi$. This is semantic equivalence.

Let's look at (1). You got to the formula $true{\bf U} (\psi\vee \neg \phi)$. Now, this holds in a computation $\pi$ iff there exists $i\ge 0$ such that $\pi^i\models \psi\vee \neg \phi$. Assume now that $i$ is minimal with respect to this property, and consider the computations $\pi^j$ for $jthere exists a computation $\pi$ that satisfies one but not the other.

Hint: It could be the case that $\phi$ holds only finitely many times, but $\psi$ does not hold after $\phi$.

StackExchange Computer Science Q#66954, answer score: 5