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