λf. λm. (∀ i, i ≤ m ⇒ (f i) ≤ m) ∧ (injn f m)

Definition permut : (nat.nat -> nat.nat) -> nat.nat -> Prop := fun (f:(nat.nat -> nat.nat)) => fun (m:nat.nat) => connectives.And (forall (i:nat.nat), (nat.le i m) -> nat.le (f i) m) (injn f m)

definition permut : (nat -> nat) -> nat -> Prop := \lambda f : nat -> nat. \lambda m : nat. (And) (\forall (i:nat). ((le) i m) -> (le) (f i) m) ((injn) f m)

def permut : ((nat.nat) -> nat.nat) -> (nat.nat) -> Prop := fun (f : (nat.nat) -> nat.nat) , fun (m : nat.nat) , (((connectives.And) ) (forall (i:nat.nat) , ((((nat.le_) ) (i)) (m)) -> (((nat.le_) ) ((f) (i))) (m))) ((((permutation.injn) ) (f)) (m))

permut : [[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat] -> [nat_sttfa_th.sttfa_nat -> bool]] = (LAMBDA(f:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(LAMBDA(m:nat_sttfa_th.sttfa_nat):connectives_sttfa_th.sttfa_And((FORALL(i:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.le(i)(m) => nat_sttfa_th.le(f(i))(m))))(permutation_sttfa.injn(f)(m))))

Printing for OpenTheory is not working at the moment.