proposition: Lemma union_disj1 : forall (x : Elt) (a b : Ensf), dans x (union_disj a b) -> (exists y : Elt, dans y a /\ x = injgauche y :>Elt) \/ (exists y : Elt, dans y b /\ x = injdroite y :>Elt).
proof: Proof. unfold union_disj in |- *. intros. cut (dans x (map injgauche a) \/ dans x (map injdroite b)). 2: auto. intro H0; elim H0; clear H0. intro; left. apply dans_map; auto. intro; right. apply dans_map; auto. Qed.
imports: Ensf_types Ensf_dans Ensf_union Ensf_couple Ensf_inclus Ensf_map