FStar.Map provides a polymorphic, partial map from keys to
values, where keys support decidable equality.
m:Map.t key value is a partial map from key to value
A distinctive feature of the library is in its model of partiality.
A map can be seen as a pair of: 1. a total map key -> Tot value 2. a set of keys that record the domain of the map
* Extensional equality **