E677 forces every left multiplication to be bijective

For every universe u, finite type $\alpha:\mathrm{Type}\,u$ equipped with a Fintype instance (possibly empty), arbitrary binary operation $\operatorname{op}:\alpha\to\alpha\to\alpha$, and proposition h asserting that for all $a,b\in\alpha$, $a=\operatorname{op}\bigl(b,\operatorname{op}(a,\operatorname{op}(\operatorname{op}(b,a),b))\bigr)$, and every $y\in\alpha$, the unary map $x\mapsto\operatorname{op}(y,x)$ is bijective from $\alpha$ to $\alpha$: it is injective, so $\operatorname{op}(y,p)=\operatorname{op}(y,q)$ implies $p=q$, and surjective, so every $z\in\alpha$ has some $p\in\alpha$ with $\operatorname{op}(y,p)=z$; when $\alpha$ is empty, the quantification over y is vacuous.