proposition: Lemma lookup_natset_to_bools sz X i β : i < sz → natset_to_bools sz X !! i = Some β ↔ (i ∈ X ↔ β = true).
proof: Proof. unfold natset_to_bools, elem_of, mapset_elem_of, lookup at 2, natmap_lookup; simpl. intros. destruct (mapset_car X) as [l ?]; simpl. destruct (l !! i) as [mu|] eqn:Hmu; simpl. { rewrite lookup_resize, list_lookup_fmap, Hmu by (rewrite ?fmap_length; eauto using lookup_lt_Some). destruct mu as [[]|], β; simpl; intuition congruence. } rewrite lookup_resize_new by (rewrite ?fmap_length; eauto using lookup_ge_None_1); destruct β; intuition congruence. Qed.
imports: stdpp(fin_maps mapset) stdpp(options)