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

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

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

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

injective_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.injn(permutation_sttfa.invert_permut(n)(f))(n))))

Printing for OpenTheory is not working at the moment.