proposition: Lemma filterP_eq_cons A f (l l': list A) x: filterP f l = x :: l' -> f x /\ exists p p', l = p ++ x :: p' /\ (forall x (IN: In x p) (COND: f x), False) /\ l' = filterP f p'.
proof: Proof. induction l; ins; desf. by splits; ins; eexists nil; eexists; splits; ins; desf; eauto. eapply IHl in H; desc; splits; ins; desf. eexists (_ :: _); eexists; splits; ins; desf; eauto. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation