Aop 1

Theorem timesA : Aop (nat.nat) (nat.S nat.O).

theorem timesA : (Aop) (nat) ((S) (O) ).

theorem timesA : ((bigops.Aop) (nat.nat)) (((nat.S) ) ((nat.O) )).

timesA : LEMMA bigops_sttfa.Aop[nat_sttfa_th.sttfa_nat](nat_sttfa_th.sttfa_S(nat_sttfa_th.sttfa_O))

Printing for OpenTheory is not working at the moment.