Let $\mathfrak{g}$ be a simple Lie algebra over $\mathbb{C}$. The $\mathfrak{g}$-current (Lie) algebra is $\mathfrak{g} \otimes \mathbb{C}[t]$, with Lie bracket given by $[a \otimes t^m, b \otimes t^n] = [a, b]_\mathfrak{g} \otimes t^{m + n}$. There is an alternate presentation of the $\mathfrak{g}$-current algebra, known as the (Drinfeld) $J$ presentation. It is the Lie algebra generated by the elements $\mathfrak{g} \cup \{J(a) \mid a \in \mathfrak{g} \}$ (where $J(-)$ is a formal symbol) subject to the following relations, for all $a, b, c, d \in \mathfrak{g}$ and $\lambda, \mu \in \mathbb{C}$:
- $[a, b] = [a, b]_\mathfrak{g}$,
- $J(\lambda a + \mu b) = \lambda J(a) + \mu J(b)$,
- $[a, J(b)] = J([a, b])$,
- $[J(a), J([b, c])] + [J(b), J([c, a])] + [J(c), J([a, b])] = 0$,
- $[[J(a), J(b)], J([c, d])] + [[J(c), J(d)], J([a, b])] = 0$.
(An isomorphism is given by $a \mapsto a \otimes 1$ and $J(a) \mapsto a \otimes t$.) This presentation can be obtained from a similar $J$ presentation for Yangians (see e.g. Theorem 12.1.1 in A Guide to Quantum Groups by Chari and Pressley) by setting the quantum parameter $h$ to 0.
The definition of the $J$ presentation is often accompanied by a note that when $\mathfrak{g} \not\cong \mathfrak{sl}_2$, the fifth relation follows from the first four. A proof is outlined in some comments after Proposition 3.2 in https://arxiv.org/abs/1709.08162, but I'm not very familiar with the methods being used in the cited papers and I've had trouble understanding the argument. Is there a more elementary/direct proof -- say, one that works just with the $J$ presentation, rather than passing to another presentation?