let is_related_to (bs:list (var & typ)) (m:Map.t var typ) =
  (forall (b:var & typ).{:pattern L.memP b bs}
          L.memP b bs ==> (Map.contains m (fst b) /\
                           Map.sel m (fst b) == snd b)) /\
  
  (forall (x:var).{:pattern Map.contains m x} Map.contains m x ==> (L.memP (x, Map.sel m x) bs))
let is_related_to (bs: list (var & typ)) (m: Map.t var typ) =
(forall (b: var & typ). {:pattern L.memP b bs}
    L.memP b bs ==> (Map.contains m (fst b) /\ Map.sel m (fst b) == snd b)) /\
(forall (x: var). {:pattern Map.contains m x} Map.contains m x ==> (L.memP (x, Map.sel m x) bs))
Pulse.Typing.Env.fsti.checked
Pulse.Syntax.fst.checked Pulse.RuntimeUtils.fsti.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Tactics.Result.fsti.checked FStar.Stubs.Pprint.fsti.checked FStar.Set.fsti.checked FStar.Reflection.Typing.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Map.fsti.checked FStar.List.Tot.fst.checked FStar.Issue.fsti.checked
Pulse.Typing.Env.fsti
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 FStar.List.Tot

open Pulse.Syntax

module L = FStar.List.Tot

module RT = FStar.Reflection.Typing
module T = FStar.Tactics.V2
module Pprint = FStar.Stubs.Pprint

type binding = var & typ
type env_bindings = list binding

val env : Type0

val fstar_env (g:env) : RT.fstar_top_env

//
// most recent binding at the head of the list
//
val bindings (g:env) : env_bindings

val as_map (g:env) : Map.t var typ
val is_related_to : 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