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