show a Proper instance for dom

theories/fin_map_dom.v

@@ -119,6 +119,11 @@ Proof.
     eauto using (empty_finite (C:=D)), (union_finite (C:=D)),
     (singleton_finite (C:=D)).
 Qed.
+Global Instance dom_proper `{!Equiv A} : Proper ((≡@{M A}) ==> (≡)) (dom D).
+Proof.
+  intros m1 m2 EQm. apply elem_of_equiv. intros i.
+  rewrite !elem_of_dom, EQm. done.
+Qed.
 
 Context `{!LeibnizEquiv D}.
 Lemma dom_empty_L {A} : dom D (@empty (M A) _) = ∅.