∀ 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) ⇒ Aop nil

Axiom mk_Aop : 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)) -> Aop (A) nil

axiom mk_Aop : \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)) -> (Aop) (A) nil

axiom mk_Aop : 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))) -> ((bigops.Aop) (A)) (nil)

mk_Aop [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))))) => bigops_sttfa.Aop[A](nil))))))

Printing for OpenTheory is not working at the moment.