proposition: Lemma pred_infinite_surj {A B} (P : B → Prop) (f : A → B) : (∀ x, P x → ∃ y, f y = x) → pred_infinite P → pred_infinite (P ∘ f).
proof: Proof. intros Hf HP xs. destruct (HP (f <$> xs)) as [x [HPx Hx]]. destruct (Hf _ HPx) as [y Hf']. exists y. split. - simpl. rewrite Hf'. done. - intros Hy. apply Hx. apply elem_of_list_fmap. eauto. Qed.
imports: stdpp(finite) stdpp(options)