proposition: Lemma singl_inclus_add : forall (e : Elt) (a : Ensf), inclus (singleton e) (add e a).
proof: Proof. unfold inclus in |- *. intros e a x H. cut (x = e); auto. intro H0. rewrite H0; auto. Qed.
imports: Ensf_types Ensf_dans Ensf_union Ensf_produit