Negation of the semantics of the Until operator in LTL
First, note that you did not really get the "first part the the expression correct". The first formula is, roughly, of the form

$$
\forall i, (p(i) \lor q(i))
$$
while the second one is of the form
$$
r \lor (\forall k, p(k))
$$
Note the different bracketing.

That being said, you have two definitions for the semantics of the release operator, and you want to prove them equivalent. So far, you tried to manipulate those formulae according to standard logical rules (a correct approach), but failed to do so. Indeed, as far as I can see, that approach can not succeed. The nice news is that you do not need to use that approach: in order to prove that definition $A$ and $B$ are equivalent, you can also write two distinct proofs, one for $A \implies B$ and one for $B \implies A$. In writing such proofs, you can leverage all the known results from mathematics, not just those allowing formula manipulation.

In your specific case, you will need to use the well-ordering property of natural numbers, stating that any non-empty set of naturals must have a least element. Let me sketch a part of the proof.

Assume your first definition, and let's prove the second one.
We consider two cases. 


If $\pi[k] \models \psi$ for all $k$, then the second definition is trivially true.
Otherwise, $\pi[k] \not\models \psi$ for some $k$. This means that the set of natural numbers $\{k|\pi[k] \not\models \psi\}$ is not empty, hence has a least element -- let $m$ be that element. This means that $m$ satisfies $\pi[m] \not\models \psi$, and that (minimality) $\forall n&lt;m, \pi[n] \models \psi$. Now, using the hypothesis, we can obtain that $\exists j&lt;m, \pi[j]\models\phi$. From this and minimality we obtain the thesis.


Note that you still need to prove the other direction.