proposition: Lemma filterP_eq_nil A f (l: list A): filterP f l = nil <-> forall x (IN: In x l) (COND: f x), False.
proof: Proof. split; ins. * enough (In x nil) by done. rewrite <- H; apply in_filterP_iff; eauto. * induction l; ins; desf; eauto; exfalso; eauto. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation