2 (** {1 Injections, surjections and bijections} *)
11 axiom Inj : forall x : a. from(to_ x) = x
13 goal G1 : forall x y : a. to_(x)=to_(y) -> x = y
14 goal G2 : forall y : a. exists x : v. from(x)=y
25 clone export Injective with type v = a, type a = v,
26 function to_ = from, function from = to_, axiom Inj
32 clone export Injective
33 clone Surjective as S with type v = v, type a = a,
34 function to_ = to_, function from = from, axiom Inj