nat.nat → (nat.nat → nat.nat) → nat.nat → nat.nat

Parameter invert_permut_body : nat.nat -> (nat.nat -> nat.nat) -> nat.nat -> nat.nat

axiom invert_permut_body : nat -> (nat -> nat) -> nat -> nat

constant invert_permut_body : (nat.nat) -> ((nat.nat) -> nat.nat) -> (nat.nat) -> nat.nat

invert_permut_body : [nat_sttfa_th.sttfa_nat -> [[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat] -> [nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]]]

Printing for OpenTheory is not working at the moment.