proposition: Lemma elem_of_bools_to_natset βs i : i ∈ bools_to_natset βs ↔ βs !! i = Some true.
proof: Proof. rewrite bools_to_natset_unfold; unfold elem_of, mapset_elem_of; simpl. rewrite list_to_natmap_spec, list_lookup_fmap. destruct (βs !! i) as [[]|]; compute; intuition congruence. Qed.
imports: stdpp(fin_maps mapset) stdpp(options)