let dom (ss:ss_t) = Map.domain (as_map ss)
let dom (ss: ss_t) =
Map.domain (as_map ss)
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 FStar.Map.domain Pulse.Syntax.Base.var Pulse.Syntax.Base.term Pulse.Checker.Prover.Substs.as_map FStar.Set.set
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
val dom : ss: Pulse.Checker.Prover.Substs.ss_t -> FStar.Set.set Pulse.Syntax.Base.var
ss: Pulse.Checker.Prover.Substs.ss_t -> FStar.Set.set Pulse.Syntax.Base.var