E677 implies E255 for finite magmas

For every universe u, finite possibly empty type $\alpha:\mathrm{Type}\,u$, and arbitrary binary operation $\operatorname{op}:\alpha\to\alpha\to\alpha$, if every $a,b\in\alpha$ satisfy $a=\operatorname{op}\bigl(b,\operatorname{op}(a,\operatorname{op}(\operatorname{op}(b,a),b))\bigr)$, then every $x\in\alpha$ satisfies $x=\operatorname{op}\bigl(\operatorname{op}(\operatorname{op}(x,x),x),x\bigr)$; for an empty $\alpha$, both the hypothesis and conclusion are universal propositions holding vacuously.