proposition: Lemma filter_elements s f : elements (filter f s) = List.filter f (elements s).
proof: Proof. unfold filter. now rewrite treeify_elements, filter_aux_elements, app_nil_r. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat