proposition: Lemma dans_singleprod2 : forall (x x0 : Elt) (b : Ensf), dans x (singleprod x0 b) -> exists y : Elt, x = couple x0 y /\ dans y b.
proof: Proof. intros x x0. simple induction b. intro. apply (dans_empty_imp_P x); auto. intros a b0 H. simpl in |- *. intro. cut (couple x0 a = x :>Elt \/ dans x (singleprod x0 b0)). 2: apply dans_add; auto. intro H1; elim H1; clear H1. intro. exists a; auto. intro. cut (exists y : Elt, x = couple x0 y /\ dans y b0); auto. intro H2; elim H2; clear H2. intros. exists x1. elim H2; clear H2. intros. split; auto. Qed.
imports: Ensf_types Ensf_dans Ensf_union Ensf_couple