let sel (ss:ss_t) (x:var { contains ss x }) = Map.sel (as_map ss) x
let sel (ss: ss_t) (x: var{contains ss x}) =
Map.sel (as_map ss) x
Pulse.Checker.Prover.Substs.fsti.checked
Pulse.Typing.Env.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.fst.checked prims.fst.checked FStar.Tactics.fst.checked FStar.Set.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Map.fsti.checked FStar.List.Tot.fst.checked
Pulse.Checker.Prover.Substs.fsti
Pulse.Checker.Prover.Substs.ss_t Pulse.Syntax.Base.var Prims.b2t Pulse.Checker.Prover.Substs.contains FStar.Map.sel Pulse.Syntax.Base.term Pulse.Checker.Prover.Substs.as_map
module Pulse.Checker.Prover.Substs

open FStar.List.Tot

open Pulse.Syntax
open Pulse.Typing.Env
open Pulse.Typing

module L = FStar.List.Tot
module T = FStar.Tactics

module Env = Pulse.Typing.Env

val ss_t : Type0

val as_map (ss:ss_t) : Map.t var term

let dom (ss:ss_t) = Map.domain (as_map ss)
val sel : ss: Pulse.Checker.Prover.Substs.ss_t ->
    x: Pulse.Syntax.Base.var{Pulse.Checker.Prover.Substs.contains ss x}
  -> Pulse.Syntax.Base.term

    ss: Pulse.Checker.Prover.Substs.ss_t ->
    x: Pulse.Syntax.Base.var{Pulse.Checker.Prover.Substs.contains ss x}
  -> Pulse.Syntax.Base.term