∀ n, leibniz (filter_nat_type leb_body n) (leb n)

Theorem sym_eq_leb : forall (n:nat), leibniz.leibniz (nat -> bool.bool) (filter_nat_type (nat -> bool.bool) leb_body n) (leb n).

theorem sym_eq_leb : \forall (n:nat). (leibniz) (nat -> bool) ((filter_nat_type) (nat -> bool) (leb_body) n) ((leb) n).

theorem sym_eq_leb : forall (n:nat.nat) , (((leibniz.leibniz) ((nat.nat) -> bool.bool)) ((((nat.filter_nat_type) ((nat.nat) -> bool.bool)) ((nat.leb_body) )) (n))) (((nat.leb) ) (n)).

sym_eq_leb : LEMMA (FORALL(n:nat_sttfa.sttfa_nat):leibniz_sttfa_th.leibniz[[nat_sttfa.sttfa_nat -> bool_sttfa_th.sttfa_bool]](nat_sttfa.filter_nat_type[[nat_sttfa.sttfa_nat -> bool_sttfa_th.sttfa_bool]](nat_sttfa.leb_body)(n))(nat_sttfa.leb(n)))

Printing for OpenTheory is not working at the moment.