val t : k: Prims.eqtype -> v: Type -> Type
let t (k: eqtype) (v: Type) = k ^-> v
module Spec.Map

let op_Hat_Subtraction_Greater = FStar.FunctionalExtensionality.op_Hat_Subtraction_Greater
/
prims.fst.checked FStar.Pervasives.fsti.checked FStar.FunctionalExtensionality.fsti.checked
Spec.Map.fst
k: Prims.eqtype -> v: Type -> Type
Prims.eqtype Spec.Map.op_Hat_Subtraction_Greater
let t (k: eqtype) (v: Type) =
  
k ^-> v