nat.filter_nat_type
∀ return, (nat.nat → return) → nat.nat → return
Parameter filter_nat_type : forall (return_:Type), (nat -> return_) -> nat -> return_
axiom filter_nat_type : \forall return_ : Type[0] . (nat -> return_) -> nat -> return_
constant filter_nat_type : forall (return : Type) , ((nat.nat) -> return) -> (nat.nat) -> return
filter_nat_type [return:TYPE+] : [[nat_sttfa.sttfa_nat -> return] -> [nat_sttfa.sttfa_nat -> return]]
Printing for OpenTheory is not working at the moment.