proposition: Lemma union_g : forall (x : Elt) (a b : Ensf), dans x a -> dans x (union a b).
proof: Proof. intro x. simple induction a. intros. apply (dans_empty_imp_P x); auto. intros a0 b H b0. simpl in |- *. intro. cut (a0 = x :>Elt \/ dans x b). 2: apply dans_add; auto. intro H1; elim H1; clear H1. intro H1. rewrite H1; auto. auto. Qed.
imports: Ensf_types Ensf_dans