λf. ∀ x y, (f x) = (f y) ⇒ x = y

Definition injective : forall (A:Type), forall (B:Type), (A -> B) -> Prop := fun (A:Type) => fun (B:Type) => fun (f:(A -> B)) => forall (x:A), forall (y:A), (logic.eq (B) (f x) (f y)) -> logic.eq (A) x y

definition injective : \forall A : Type[0] . \forall B : Type[0] . (A -> B) -> Prop := \lambda A : Type[0]. \lambda B : Type[0]. \lambda f : A -> B. \forall (x:A). \forall (y:A). ((eq) (B) (f x) (f y)) -> (eq) (A) x y

def injective : forall (A : Type) , forall (B : Type) , ((A) -> B) -> Prop := fun (A : Type) , fun (B : Type) , fun (f : (A) -> B) , forall (x:A) , forall (y:A) , ((((logic.eq_) (B)) ((f) (x))) ((f) (y))) -> (((logic.eq_) (A)) (x)) (y)

injective [A:TYPE+,B:TYPE+] : [[A -> B] -> bool] = (LAMBDA(f:[A -> B]):(FORALL(x:A):(FORALL(y:A):(logic_sttfa_th.eq[B](f(x))(f(y)) => logic_sttfa_th.eq[A](x)(y)))))

Printing for OpenTheory is not working at the moment.