∀ n, leibniz 1 (exp_body n O)

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

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

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

sym_eq_exp_body_O : LEMMA (FORALL(n:nat_sttfa_th.sttfa_nat):leibniz_sttfa_th.leibniz[nat_sttfa_th.sttfa_nat](nat_sttfa_th.sttfa_S(nat_sttfa_th.sttfa_O))(exp_sttfa.exp_body(n)(nat_sttfa_th.sttfa_O)))

Printing for OpenTheory is not working at the moment.