proposition: Lemma map_inclus : forall (a b : Ensf) (f : Elt -> Elt), inclus a b -> inclus (map f a) (map f b).
proof: Proof. unfold inclus in |- *. intros. cut (exists y : Elt, dans y a /\ x = f y :>Elt). 2: apply dans_map; auto. intro Ht; elim Ht; clear Ht; intros y Ht; elim Ht; clear Ht; intros. cut (dans y b); auto. intro. replace x with (f y); auto. Qed.
imports: Ensf_types Ensf_dans Ensf_union Ensf_inclus