proposition: Lemma filterP_eq_app A f (l l' l'': list A) : filterP f l = l' ++ l'' -> exists p p', l = p ++ p' /\ l' = filterP f p /\ l'' = filterP f p'.
proof: Proof. revert l'; induction l; ins; desf. { destruct l'; ins; desf; exists nil, nil; ins. } destruct l'; ins; desf. eexists nil, (_ :: _); splits; ins; desf. all: apply IHl in H; desf; eexists (_ :: _), _; splits; ins; desf. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation