proposition: Lemma natset_to_bools_union sz X1 X2 : natset_to_bools sz (X1 ∪ X2) = natset_to_bools sz X1 ||* natset_to_bools sz X2.
proof: Proof. apply list_eq; intros i; rewrite lookup_zip_with. destruct (decide (i < sz)); [|by rewrite !lookup_natset_to_bools_ge by lia]. apply option_eq; intros β. rewrite lookup_natset_to_bools, elem_of_union by done; intros. destruct (decide (i ∈ X1)), (decide (i ∈ X2)); repeat first [ rewrite (λ X H, proj2 (lookup_natset_to_bools_true sz X i H)) by done | rewrite (λ X H, proj2 (lookup_natset_to_bools_false sz X i H)) by done]; destruct β; naive_solver. Qed.
imports: stdpp(fin_maps mapset) stdpp(options)