proposition: Lemma In_Image_elim : forall (A:Ensemble U) (f:U -> V), injective f -> forall x:U, In _ (Im A f) (f x) -> In _ A x.
proof: Proof. intros. elim Im_inv with A f (f x); trivial with sets. intros z C; elim C; intros InAz E. elim (H z x E); trivial with sets. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts Finite_sets_facts