∀ return, leibniz (return O) (filter_nat_type return O)

Theorem sym_eq_filter_nat_type_O : forall return_type, forall (return_:(nat -> return_type)), leibniz.leibniz (return_type) (return_ O) (filter_nat_type (return_type) return_ O).

theorem sym_eq_filter_nat_type_O : \forall return_type. \forall (return_:nat -> return_type). (leibniz) (return_type) (return_ (O) ) ((filter_nat_type) (return_type) return_ (O) ).

theorem sym_eq_filter_nat_type_O : forall (return_type : Type) , forall (return:(nat.nat) -> return_type) , (((leibniz.leibniz) (return_type)) ((return) ((nat.O) ))) ((((nat.filter_nat_type) (return_type)) (return)) ((nat.O) )).

sym_eq_filter_nat_type_O [return_type:TYPE+] : LEMMA (FORALL(return:[nat_sttfa.sttfa_nat -> return_type]):leibniz_sttfa_th.leibniz[return_type](return(nat_sttfa.sttfa_O))(nat_sttfa.filter_nat_type[return_type](return)(nat_sttfa.sttfa_O)))

Printing for OpenTheory is not working at the moment.