proposition: Lemma natset_to_bools_to_natset βs sz : natset_to_bools sz (bools_to_natset βs) = resize sz false βs.
proof: Proof. apply list_eq; intros i. destruct (decide (i < sz)); [|by rewrite lookup_natset_to_bools_ge, lookup_resize_old by lia]. apply option_eq; intros β. rewrite lookup_natset_to_bools, elem_of_bools_to_natset by done. destruct (decide (i < length βs)). { rewrite lookup_resize by done. destruct (lookup_lt_is_Some_2 βs i) as [[]]; destruct β; naive_solver. } rewrite lookup_resize_new, lookup_ge_None_2 by lia. destruct β; naive_solver. Qed.
imports: stdpp(fin_maps mapset) stdpp(options)