∀ n, equal (exp_body n O) 1

Axiom axiom_exp_body_O : forall (n:nat.nat), connectives.equal (nat.nat) (exp_body n nat.O) (nat.S nat.O)

axiom axiom_exp_body_O : \forall (n:nat). (equal) (nat) ((exp_body) n (O) ) ((S) (O) )

axiom axiom_exp_body_O : forall (n:nat.nat) , (((connectives.equal) (nat.nat)) ((((exp.exp_body) ) (n)) ((nat.O) ))) (((nat.S) ) ((nat.O) ))

axiom_exp_body_O : AXIOM (FORALL(n:nat_sttfa_th.sttfa_nat):connectives_sttfa_th.equal[nat_sttfa_th.sttfa_nat](exp_sttfa.exp_body(n)(nat_sttfa_th.sttfa_O))(nat_sttfa_th.sttfa_S(nat_sttfa_th.sttfa_O)))

Printing for OpenTheory is not working at the moment.