equal (fact_body O) 1

Axiom axiom_fact_body_O : connectives.equal (nat.nat) (fact_body nat.O) (nat.S nat.O)

axiom axiom_fact_body_O : (equal) (nat) ((fact_body) (O) ) ((S) (O) )

axiom axiom_fact_body_O : (((connectives.equal) (nat.nat)) (((fact.fact_body) ) ((nat.O) ))) (((nat.S) ) ((nat.O) ))

axiom_fact_body_O : AXIOM connectives_sttfa_th.equal[nat_sttfa_th.sttfa_nat](fact_sttfa.fact_body(nat_sttfa_th.sttfa_O))(nat_sttfa_th.sttfa_S(nat_sttfa_th.sttfa_O))

Printing for OpenTheory is not working at the moment.