proposition: Lemma bools_to_natset_unfold βs : let f (β : bool) := if β then Some () else None in bools_to_natset βs = Mapset $ list_to_natmap $ f <$> βs.
proof: Proof. by destruct βs. Qed.
imports: stdpp(fin_maps mapset) stdpp(options)