proposition: Lemma coPset_r_finite X : set_finite (coPset_r X) → set_finite X.
proof: Proof. rewrite !coPset_finite_spec; destruct X as [t Ht]; simpl; clear Ht. induction t as [[]|]; simpl; rewrite ?coPset_finite_node, ?andb_True; tauto. Qed.
imports: stdpp(pmap gmap mapset) stdpp(options)