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

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

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

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

f_invert_permut : 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.permut(f)(n) => logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](f(permutation_sttfa.invert_permut(n)(f)(m)))(m))))))

Printing for OpenTheory is not working at the moment.