proposition: Lemma inter_dans : forall (A B : Ensf) (x : Elt), inter A B empty -> dans x A -> ~ dans x B.
proof: Proof. unfold inter in |- *. intros. elim H; clear H; intros H Ht; elim Ht; clear Ht; intros H1 H2. red in |- *; intro. cut (dans x empty); auto. intro. apply dans_empty_imp_P with x; auto. Qed.
imports: Ensf_types Ensf_dans Ensf_union Ensf_inclus