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