proposition: Lemma sym_inter : forall A B C : Ensf, inter A B C -> inter B A C.
proof: Proof. unfold inter in |- *. intros. elim H; clear H; intros H Ht; elim Ht; clear Ht; intros H0 H1. auto. Qed.
imports: Ensf_types Ensf_dans Ensf_union Ensf_inclus