FDL > PVS > Prelude > functions > injective? : const-decl

injective?(f): bool = FORALL x1, x2 : (f(x1) = f(x2)) = > (x1 = x2);