proposition: Lemma inverse_image_surjective_injective {X Y : Type} (f : X -> Y) : surjective f -> injective (inverse_image f).
proof: Proof. intros H U V eq. apply Extensionality_Ensembles. split; red; intros; destruct (H x); subst; apply (in_inverse_image f); [ rewrite <- eq | rewrite eq ]; now constructor. Qed.
imports: FunctionProperties Ensembles EnsemblesImplicit EnsemblesSpec IndexedFamilies