leibniz (fact_body O) 1

Theorem eq_fact_body_O : leibniz.leibniz (nat.nat) (fact_body nat.O) (nat.S nat.O).

theorem eq_fact_body_O : (leibniz) (nat) ((fact_body) (O) ) ((S) (O) ).

theorem eq_fact_body_O : (((leibniz.leibniz) (nat.nat)) (((fact.fact_body) ) ((nat.O) ))) (((nat.S) ) ((nat.O) )).

eq_fact_body_O : LEMMA leibniz_sttfa_th.leibniz[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.