(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))