∀ nil op, ∀ a, (op nil a) = a ⇒ ∀ a, (op a nil) = a ⇒ ∀ a b c, (op a (op b c)) = (op (op a b) c) ⇒ ∀ a b, (op a b) = (op b a) ⇒ ACop nil

Axiom mk_ACop : forall A, forall (nil:A), forall (op:(A -> A -> A)), (forall (a:A), logic.eq (A) (op nil a) a) -> (forall (a:A), logic.eq (A) (op a nil) a) -> (forall (a:A), forall (b:A), forall (c:A), logic.eq (A) (op a (op b c)) (op (op a b) c)) -> (forall (a:A), forall (b:A), logic.eq (A) (op a b) (op b a)) -> ACop (A) nil

axiom mk_ACop : \forall A. \forall (nil:A). \forall (op:A -> A -> A). (\forall (a:A). (eq) (A) (op nil a) a) -> (\forall (a:A). (eq) (A) (op a nil) a) -> (\forall (a:A). \forall (b:A). \forall (c:A). (eq) (A) (op a (op b c)) (op (op a b) c)) -> (\forall (a:A). \forall (b:A). (eq) (A) (op a b) (op b a)) -> (ACop) (A) nil

axiom mk_ACop : forall (A : Type) , forall (nil:A) , forall (op:(A) -> (A) -> A) , (forall (a:A) , (((logic.eq_) (A)) (((op) (nil)) (a))) (a)) -> (forall (a:A) , (((logic.eq_) (A)) (((op) (a)) (nil))) (a)) -> (forall (a:A) , forall (b:A) , forall (c:A) , (((logic.eq_) (A)) (((op) (a)) (((op) (b)) (c)))) (((op) (((op) (a)) (b))) (c))) -> (forall (a:A) , forall (b:A) , (((logic.eq_) (A)) (((op) (a)) (b))) (((op) (b)) (a))) -> ((bigops.ACop) (A)) (nil)

mk_ACop [A:TYPE+] : AXIOM (FORALL(nil:A):(FORALL(op:[A -> [A -> A]]):((FORALL(a:A):logic_sttfa_th.eq[A](op(nil)(a))(a)) => ((FORALL(a:A):logic_sttfa_th.eq[A](op(a)(nil))(a)) => ((FORALL(a:A):(FORALL(b:A):(FORALL(c:A):logic_sttfa_th.eq[A](op(a)(op(b)(c)))(op(op(a)(b))(c))))) => ((FORALL(a:A):(FORALL(b:A):logic_sttfa_th.eq[A](op(a)(b))(op(b)(a)))) => bigops_sttfa.ACop[A](nil)))))))

Printing for OpenTheory is not working at the moment.