proposition: Lemma map_egal : forall (f g : Elt -> Elt) (E : Ensf), (forall x : Elt, dans x E -> f x = g x :>Elt) -> map f E = map g E :>Ensf.
proof: Proof. intros f g. simple induction E; simpl in |- *; auto. Qed.
imports: Ensf_types Ensf_dans Ensf_union Ensf_inclus