proposition: Lemma dans_map : forall (f : Elt -> Elt) (a : Ensf) (x : Elt), dans x (map f a) -> exists y : Elt, dans y a /\ x = f y.
proof: Proof. intros f. simple induction a. simpl in |- *. intros x H. absurd (dans x empty); auto. intros a0 b H x. simpl in |- *. intro. cut (f a0 = x :>Elt \/ dans x (map f b)). 2: apply dans_add; auto. intro H1; elim H1; clear H1. intro; exists a0; auto. intro. cut (exists y : Elt, dans y b /\ x = f y). intro H2; elim H2; clear H2. 2: auto. intros x0 H2; elim H2; clear H2. intros. exists x0. split; auto. Qed.
imports: Ensf_types Ensf_dans Ensf_union Ensf_inclus