proposition: Lemma coPpick_raw_elem_of t i : coPpick_raw t = Some i → e_of i t.
proof: Proof. revert i; 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)