∀ n, leibniz (exp_body n O) 1

Theorem eq_exp_body_O : forall (n:nat.nat), leibniz.leibniz (nat.nat) (exp_body n nat.O) (nat.S nat.O).

theorem eq_exp_body_O : \forall (n:nat). (leibniz) (nat) ((exp_body) n (O) ) ((S) (O) ).

theorem eq_exp_body_O : forall (n:nat.nat) , (((leibniz.leibniz) (nat.nat)) ((((exp.exp_body) ) (n)) ((nat.O) ))) (((nat.S) ) ((nat.O) )).

eq_exp_body_O : LEMMA (FORALL(n:nat_sttfa_th.sttfa_nat):leibniz_sttfa_th.leibniz[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.