proposition: Lemma dans_tq_imp : forall (x : Elt) (f : Elt -> Prop) (E : Ensf), dans x (tq f E) -> dans x E /\ f x.
proof: Proof. intros x f. simple induction E. replace (tq f empty) with empty; auto. intro. apply (dans_empty_imp_P x); auto. intros a b H. replace (tq f (add a b)) with match Pdec f a return Ensf with | left fa => add a (tq f b) | right nfa => tq f b end; auto. elim (Pdec f a). intros a0 H0. cut (a = x :>Elt \/ dans x (tq f b)). 2: apply dans_add; auto. intro H1; elim H1; clear H1. intro H1; rewrite <- H1; auto. intro. cut (dans x b /\ f x); auto. intro H2; elim H2; auto. intros. cut (dans x b /\ f x); auto. intro H1; elim H1; auto. Qed.
imports: Ensf