proposition: Lemma elem_of_coPset_to_Pset X i : set_finite X → i ∈ coPset_to_Pset X ↔ i ∈ X.
proof: Proof. rewrite coPset_finite_spec; destruct X as [t Ht]. change (coPset_finite t → coPset_to_Pset_raw t !! i = Some () ↔ e_of i t). clear Ht; revert i; induction t as [[]|[] l IHl r IHr]; intros [i|i|]; simpl; rewrite ?andb_True, ?pmap.Pmap_lookup_PNode; naive_solver. Qed.
imports: stdpp(pmap gmap mapset) stdpp(options)