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