Commit bdd1e381 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen

Add FMap.ext_eq

parent 79abd5bf
Pipeline #20417 passed with stage
in 9 minutes and 43 seconds
......@@ -40,6 +40,11 @@ Module FMap.
Section Theories.
Context {K V : Type} `{countable.Countable K}.
Lemma ext_eq (m1 m2 : FMap K V) :
(forall k, FMap.find k m1 = FMap.find k m2) ->
m1 = m2.
Proof. apply fin_maps.map_eq. Qed.
Lemma of_elements_eq (m : FMap K V) :
of_list (elements m) = m.
Proof. apply fin_maps.list_to_map_to_list. Qed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment