∀ f n m, m ≤ n ⇒ injn f n ⇒ (invert_permut n f (f m)) = m

Theorem invert_permut_f : forall (f:(nat.nat -> nat.nat)), forall (n:nat.nat), forall (m:nat.nat), (nat.le m n) -> (injn f n) -> logic.eq (nat.nat) (invert_permut n f (f m)) m.

theorem invert_permut_f : \forall (f:nat -> nat). \forall (n:nat). \forall (m:nat). ((le) m n) -> ((injn) f n) -> (eq) (nat) ((invert_permut) n f (f m)) m.

theorem invert_permut_f : forall (f:(nat.nat) -> nat.nat) , forall (n:nat.nat) , forall (m:nat.nat) , ((((nat.le_) ) (m)) (n)) -> ((((permutation.injn) ) (f)) (n)) -> (((logic.eq_) (nat.nat)) (((((permutation.invert_permut) ) (n)) (f)) ((f) (m)))) (m).

invert_permut_f : LEMMA (FORALL(f:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(FORALL(n:nat_sttfa_th.sttfa_nat):(FORALL(m:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.le(m)(n) => (permutation_sttfa.injn(f)(n) => logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](permutation_sttfa.invert_permut(n)(f)(f(m)))(m))))))

Printing for OpenTheory is not working at the moment.