proposition: Lemma imp_dans_tq : forall (x : Elt) (f : Elt -> Prop) (E : Ensf), dans x E -> f x -> dans x (tq f E).
proof: Proof. intros x f. simple induction E. intro. apply (dans_empty_imp_P x); auto. intros a b H H0 x0. 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). intro. cut (a = x :>Elt \/ dans x b). 2: apply dans_add; auto. intro H1; elim H1; clear H1. intro H1; rewrite H1; auto. auto. intro. cut (a = x :>Elt \/ dans x b). 2: apply dans_add; auto. intro H1; elim H1; clear H1. intro. absurd (f a); auto. rewrite H1; auto. auto. Qed.
imports: Ensf