proposition: Lemma filterP_set_equiv A (f f' : A -> Prop) (EQ: f ≡₁ f') (l : list A) : filterP f l = filterP f' l.
proof: Proof. induction l; ins; desf; f_equal; firstorder. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation