∀ n m, leibniz (filter_nat_type (exp_body n) m) (n ^ m)

Theorem sym_eq_exp : forall (n:nat.nat), forall (m:nat.nat), leibniz.leibniz (nat.nat) (nat.filter_nat_type (nat.nat) (exp_body n) m) (exp n m).

theorem sym_eq_exp : \forall (n:nat). \forall (m:nat). (leibniz) (nat) ((filter_nat_type) (nat) ((exp_body) n) m) ((exp) n m).

theorem sym_eq_exp : forall (n:nat.nat) , forall (m:nat.nat) , (((leibniz.leibniz) (nat.nat)) ((((nat.filter_nat_type) (nat.nat)) (((exp.exp_body) ) (n))) (m))) ((((exp.exp) ) (n)) (m)).

sym_eq_exp : LEMMA (FORALL(n:nat_sttfa_th.sttfa_nat):(FORALL(m:nat_sttfa_th.sttfa_nat):leibniz_sttfa_th.leibniz[nat_sttfa_th.sttfa_nat](nat_sttfa_th.filter_nat_type[nat_sttfa_th.sttfa_nat](exp_sttfa.exp_body(n))(m))(exp_sttfa.sttfa_exp(n)(m))))

Printing for OpenTheory is not working at the moment.