proposition: Lemma difference_finite_inv X Y `{∀ x, Decision (x ∈ Y)} : set_finite Y → set_finite (X ∖ Y) → set_finite X.
proof: Proof. intros [l ?] [k ?]; exists (l ++ k). intros x ?; destruct (decide (x ∈ Y)); rewrite elem_of_app; set_solver. Qed.
imports: stdpp(finite) stdpp(options)