proposition: Lemma lookup_natset_to_bools_false sz X i : i < sz → natset_to_bools sz X !! i = Some false ↔ i ∉ X.
proof: Proof. intros. rewrite lookup_natset_to_bools by done. naive_solver. Qed.
imports: stdpp(fin_maps mapset) stdpp(options)