∀ 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.