fact.sym_eq_fact_body_O
leibniz 1 (fact_body O)
Theorem sym_eq_fact_body_O : leibniz.leibniz (nat.nat) (nat.S nat.O) (fact_body nat.O).
theorem sym_eq_fact_body_O : (leibniz) (nat) ((S) (O) ) ((fact_body) (O) ).
theorem sym_eq_fact_body_O : (((leibniz.leibniz) (nat.nat)) (((nat.S) ) ((nat.O) ))) (((fact.fact_body) ) ((nat.O) )).
sym_eq_fact_body_O : LEMMA leibniz_sttfa_th.leibniz[nat_sttfa_th.sttfa_nat](nat_sttfa_th.sttfa_S(nat_sttfa_th.sttfa_O))(fact_sttfa.fact_body(nat_sttfa_th.sttfa_O))
Printing for OpenTheory is not working at the moment.