∀ f n, permut f n ⇒ permut (invert_permut n f) n

Theorem permut_invert_permut : forall (f:(nat.nat -> nat.nat)), forall (n:nat.nat), (permut f n) -> permut (invert_permut n f) n.

theorem permut_invert_permut : \forall (f:nat -> nat). \forall (n:nat). ((permut) f n) -> (permut) ((invert_permut) n f) n.

theorem permut_invert_permut : forall (f:(nat.nat) -> nat.nat) , forall (n:nat.nat) , ((((permutation.permut) ) (f)) (n)) -> (((permutation.permut) ) ((((permutation.invert_permut) ) (n)) (f))) (n).

permut_invert_permut : LEMMA (FORALL(f:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(FORALL(n:nat_sttfa_th.sttfa_nat):(permutation_sttfa.permut(f)(n) => permutation_sttfa.permut(permutation_sttfa.invert_permut(n)(f))(n))))

Printing for OpenTheory is not working at the moment.