λf. λn. ∀ i j, i ≤ n ⇒ j ≤ n ⇒ (f i) = (f j) ⇒ i = j

Definition injn : (nat.nat -> nat.nat) -> nat.nat -> Prop := fun (f:(nat.nat -> nat.nat)) => fun (n:nat.nat) => forall (i:nat.nat), forall (j:nat.nat), (nat.le i n) -> (nat.le j n) -> (logic.eq (nat.nat) (f i) (f j)) -> logic.eq (nat.nat) i j

definition injn : (nat -> nat) -> nat -> Prop := \lambda f : nat -> nat. \lambda n : nat. \forall (i:nat). \forall (j:nat). ((le) i n) -> ((le) j n) -> ((eq) (nat) (f i) (f j)) -> (eq) (nat) i j

def injn : ((nat.nat) -> nat.nat) -> (nat.nat) -> Prop := fun (f : (nat.nat) -> nat.nat) , fun (n : nat.nat) , forall (i:nat.nat) , forall (j:nat.nat) , ((((nat.le_) ) (i)) (n)) -> ((((nat.le_) ) (j)) (n)) -> ((((logic.eq_) (nat.nat)) ((f) (i))) ((f) (j))) -> (((logic.eq_) (nat.nat)) (i)) (j)

injn : [[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(n:nat_sttfa_th.sttfa_nat):(FORALL(i:nat_sttfa_th.sttfa_nat):(FORALL(j:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.le(i)(n) => (nat_sttfa_th.le(j)(n) => (logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](f(i))(f(j)) => logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](i)(j))))))))

Printing for OpenTheory is not working at the moment.