proposition: Lemma coPset_finite_spec X : set_finite X ↔ coPset_finite (`X).
proof: Proof. destruct X as [t Ht]. unfold set_finite, elem_of at 1, coPset_elem_of; simpl; clear Ht; split. - induction t as [b|b l IHl r IHr]; simpl. { destruct b; simpl; [intros [l Hl]|done]. by apply (infinite_is_fresh l), Hl. } intros [ll Hll]; rewrite andb_True; split. + apply IHl; exists (omap (maybe (~0)) ll); intros i. rewrite elem_of_list_omap; intros; exists (i~0); auto. + apply IHr; exists (omap (maybe (~1)) ll); intros i. rewrite elem_of_list_omap; intros; exists (i~1); auto. - induction t as [b|b l IHl r IHr]; simpl; [by exists []; destruct b|]. rewrite andb_True; intros [??]; destruct IHl as [ll ?], IHr as [rl ?]; auto. exists ([1] ++ ((~0) <$> ll) ++ ((~1) <$> rl))%list; intros [i|i|]; simpl; rewrite elem_of_cons, elem_of_app, !elem_of_list_fmap; naive_solver. Qed.
imports: stdpp(pmap gmap mapset) stdpp(options)