proposition: Lemma coPpick_elem_of X : ¬set_finite X → coPpick X ∈ X.
proof: Proof. destruct X as [t ?]; unfold coPpick; destruct (coPpick_raw _) as [j|] eqn:?. - by intros; apply coPpick_raw_elem_of. - by intros []; apply coPset_finite_spec, coPpick_raw_None. Qed.
imports: stdpp(pmap gmap mapset) stdpp(options)