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