val map_eq (#k #v: _) (m0 m1: t k v)
    : Lemma (requires forall key. m0 key == m1 key) (ensures m0 == m1)
val map_eq (#k #v: _) (m0 m1: t k v)
    : Lemma (requires forall key. m0 key == m1 key) (ensures m0 == m1)
let map_eq #k #v (m0 m1: t k v)
  : Lemma (requires forall key. m0 key == m1 key)
          (ensures m0 == m1)
  = FStar.FunctionalExtensionality.extensionality _ _ m0 m1
module Spec.Map

let op_Hat_Subtraction_Greater = FStar.FunctionalExtensionality.op_Hat_Subtraction_Greater

let t (k: eqtype) (v: Type) = k ^-> v 
let upd #k #v (m: t k v) (key: k) (value: v) : t k v = 
  FStar.FunctionalExtensionality.on_domain k (fun key' -> if key = key' then value else m key')
/
prims.fst.checked FStar.Pervasives.fsti.checked FStar.FunctionalExtensionality.fsti.checked
Spec.Map.fst
m0: Spec.Map.t k v -> m1: Spec.Map.t k v
  -> FStar.Pervasives.Lemma (requires forall (key: k). m0 key == m1 key) (ensures m0 == m1)
Prims.eqtype Spec.Map.t FStar.FunctionalExtensionality.extensionality Prims.unit Prims.l_Forall Prims.eq2 Prims.squash Prims.Nil FStar.Pervasives.pattern
let map_eq #k #v (m0: t k v) (m1: t k v)
    : Lemma (requires forall key. m0 key == m1 key) (ensures m0 == m1) =
  
FStar.FunctionalExtensionality.extensionality _ _ m0 m1