proposition: Lemma coPpick_raw_None t : coPpick_raw t = None → coPset_finite t.
proof: Proof. induction t as [[]|[] l ? r]; intros i; simplify_eq/=; auto. destruct (coPpick_raw l); simplify_option_eq; auto. Qed.
imports: stdpp(pmap gmap mapset) stdpp(options)