proposition: Lemma filterP_eq_middle A f (l l' l'': list A) x : filterP f l = l' ++ x :: l'' -> f x /\ exists p p', l = p ++ x :: p' /\ l' = filterP f p /\ l'' = filterP f p'.
proof: Proof. ins; apply filterP_eq_app in H; desf. apply eq_sym, filterP_eq_cons in H1; desf. split; ins. eexists (_ ++ _), _; rewrite appA, filterP_app; splits; ins. apply filterP_eq_nil in H2; rewrite H2. apply app_nil_end. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation