proposition: Lemma mapset_eq (X1 X2 : mapset M) : X1 = X2 ↔ ∀ x, x ∈ X1 ↔ x ∈ X2.
proof: Proof. split; [by intros ->|]. destruct X1 as [m1], X2 as [m2]. simpl. intros E. f_equal. apply map_eq. intros i. apply option_eq. intros []. by apply E. Qed.
imports: stdpp(options)