proposition: Lemma inverse_image_surjective_singleton {X Y : Type} (f : X -> Y) (T : Ensemble X) : surjective f -> Included (inverse_image (inverse_image f) (Singleton T)) (Singleton (Im T f)).
proof: Proof. intros H U HU. destruct HU. inversion H0. subst. now rewrite inverse_image_image_surjective. Qed.
imports: FunctionProperties Ensembles EnsemblesImplicit EnsemblesSpec IndexedFamilies