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