proposition: Lemma filterP_ext A (f f' : A -> Prop) l (EQ: forall x (IN: In x l), f x <-> f' x) : filterP f l = filterP f' l.
proof: Proof. induction l; ins. specialize_full IHl; ins; eauto. specialize_full EQ; eauto. rewrite IHl; desf; tauto. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation