proposition: Lemma filter_spec s x f : Proper (X.eq==>Logic.eq) f -> (InT x (filter f s) <-> InT x s /\ f x = true).
proof: Proof. intros Hf. rewrite <- elements_spec1, filter_elements, filter_InA, elements_spec1; now auto_tc. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat