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

Question

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?