∀ n, equal (eqb n) (filter_nat_type eqb_body n)

Axiom axiom_eqb : forall (n:nat), connectives.equal (nat -> bool.bool) (eqb n) (filter_nat_type (nat -> bool.bool) eqb_body n)

axiom axiom_eqb : \forall (n:nat). (equal) (nat -> bool) ((eqb) n) ((filter_nat_type) (nat -> bool) (eqb_body) n)

axiom axiom_eqb : forall (n:nat.nat) , (((connectives.equal) ((nat.nat) -> bool.bool)) (((nat.eqb) ) (n))) ((((nat.filter_nat_type) ((nat.nat) -> bool.bool)) ((nat.eqb_body) )) (n))

axiom_eqb : AXIOM (FORALL(n:nat_sttfa.sttfa_nat):connectives_sttfa_th.equal[[nat_sttfa.sttfa_nat -> bool_sttfa_th.sttfa_bool]](nat_sttfa.eqb(n))(nat_sttfa.filter_nat_type[[nat_sttfa.sttfa_nat -> bool_sttfa_th.sttfa_bool]](nat_sttfa.eqb_body)(n)))

Printing for OpenTheory is not working at the moment.