(def-theorem left-group-equation
*"forall(a,b:gg,
forsome(x:gg, x mul a = b and forall(y:gg, y mul a = b implies x = y)))"*
(theory groups)
(usages transportable-macete)
(proof
(
direct-inference
(instantiate-existential (*"b mul inv(a)"*))
simplify
(force-substitution *"b"* *"y_$0 mul a"* (0))
(weaken (0))
simplify
)))

(def-theorem right-group-equation
left-group-equation
(theory groups)
(usages transportable-macete)
(translation mul-reverse)
(proof existing-theorem))

(def-theorem left-mul-macete
action-macete
(theory groups)
(usages transportable-macete)
(translation act->left-mul)
(proof existing-theorem))

(def-theorem right-mul-macete
action-macete
(theory groups)
(usages transportable-macete)
(translation act->right-mul)
(proof existing-theorem))