let related (bs:list (var & typ)) (m:Map.t var typ) =
  (forall (b:var & typ).
          L.memP b bs ==> (Map.contains m (fst b) /\
                           Map.sel m (fst b) == snd b)) /\
  
  (forall (x:var). Map.contains m x ==> (List.Tot.memP (x, Map.sel m x) bs))
let related (bs: list (var & typ)) (m: Map.t var typ) =
(forall (b: var & typ). L.memP b bs ==> (Map.contains m (fst b) /\ Map.sel m (fst b) == snd b)) /\
(forall (x: var). Map.contains m x ==> (List.Tot.memP (x, Map.sel m x) bs))
Pulse.Typing.Env.fst.checked
Pulse.Syntax.Printer.fsti.checked Pulse.Syntax.fst.checked Pulse.RuntimeUtils.fsti.checked Pulse.Config.fsti.checked prims.fst.checked FStar.Stubs.Pprint.fsti.checked FStar.String.fsti.checked FStar.Set.fsti.checked FStar.Sealed.fsti.checked FStar.Reflection.Typing.fsti.checked FStar.Reflection.fst.checked FStar.Range.fsti.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Map.fsti.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.Issue.fsti.checked FStar.IndefiniteDescription.fsti.checked FStar.Ghost.fsti.checked
Pulse.Typing.Env.fst
Prims.list FStar.Pervasives.Native.tuple2 Pulse.Syntax.Base.var Pulse.Syntax.Base.typ FStar.Map.t Prims.l_and Prims.l_Forall Prims.l_imp FStar.List.Tot.Base.memP Prims.b2t FStar.Map.contains FStar.Pervasives.Native.fst Prims.eq2 FStar.Map.sel FStar.Pervasives.Native.snd FStar.Pervasives.Native.Mktuple2 Prims.logical
module Pulse.Typing.Env

open Pulse.Syntax

module G = FStar.Ghost
module L = FStar.List.Tot

module R = FStar.Reflection
module RT = FStar.Reflection.Typing
module RU = Pulse.RuntimeUtils
open FStar.List.Tot

type bmap = m:Map.t var typ {
  forall (x:var). (~ (Map.contains m x)) ==> (Map.sel m x == tm_unknown)
}
val related : bs: Prims.list (Pulse.Syntax.Base.var * Pulse.Syntax.Base.typ) ->
    m: FStar.Map.t Pulse.Syntax.Base.var Pulse.Syntax.Base.typ
  -> Prims.logical

    bs: Prims.list (Pulse.Syntax.Base.var * Pulse.Syntax.Base.typ) ->
    m: FStar.Map.t Pulse.Syntax.Base.var Pulse.Syntax.Base.typ
  -> Prims.logical