proposition: Lemma union_inclus : forall a b c : Ensf, inclus a c -> inclus b c -> inclus (union a b) c.
proof: Proof. unfold inclus in |- *. intros. cut (dans x a \/ dans x b); auto. intro H2; elim H2; auto. Qed.
imports: Ensf_types Ensf_dans Ensf_union Ensf_produit