proposition: Lemma size_union X Y : X ## Y → size (X ∪ Y) = size X + size Y.
proof: Proof. intros. unfold size, set_size. simpl. rewrite <-app_length. apply Permutation_length, NoDup_Permutation. - apply NoDup_elements. - apply NoDup_app; repeat split; try apply NoDup_elements. intros x; rewrite !elem_of_elements; set_solver. - intros. by rewrite elem_of_app, !elem_of_elements, elem_of_union. Qed.
imports: stdpp(relations) stdpp(options)