proposition: Lemma inclus_tq : forall (f : Elt -> Prop) (a : Ensf), inclus (tq f a) a.
proof: Proof. unfold inclus in |- *. intros. cut (dans x a /\ f x); auto. 2: apply dans_tq_imp; auto. intro H0; elim H0; auto. Qed.
imports: Ensf