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