proposition: Lemma bools_to_natset_union βs1 βs2 : length βs1 = length βs2 → bools_to_natset (βs1 ||* βs2) = bools_to_natset βs1 ∪ bools_to_natset βs2.
proof: Proof. rewrite <-Forall2_same_length; intros Hβs. apply set_eq. intros i. rewrite elem_of_union, !elem_of_bools_to_natset. revert i. induction Hβs as [|[] []]; intros [|?]; naive_solver. Qed.
imports: stdpp(fin_maps mapset) stdpp(options)