let remove_map (m:ss_map) (x:var) =
  Map.restrict (Set.complement (Set.singleton x)) (Map.upd m x tm_unknown)
let remove_map (m: ss_map) (x: var) =
Map.restrict (Set.complement (Set.singleton x)) (Map.upd m x tm_unknown)
Pulse.Checker.Prover.Substs.fst.checked
Pulse.Typing.Metatheory.fsti.checked Pulse.Typing.Env.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.fst.checked prims.fst.checked FStar.Squash.fsti.checked FStar.Set.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.IndefiniteDescription.fsti.checked
Pulse.Checker.Prover.Substs.fst
Pulse.Checker.Prover.Substs.ss_map Pulse.Syntax.Base.var FStar.Map.restrict Pulse.Syntax.Base.term FStar.Set.complement FStar.Set.singleton FStar.Map.upd Pulse.Syntax.Base.tm_unknown FStar.Map.t
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 Env = Pulse.Typing.Env
module Metatheory = Pulse.Typing.Metatheory

let coerce_eq (#a #b:Type) (x:a) (_:squash (a == b)) : y:b {y == x} = x

let rec no_repeats (l:list var) : Type0 =
  match l with
  | [] -> True
  | x::tl -> (~ (L.memP x tl)) /\ no_repeats tl  

type ss_dom = l:list var { no_repeats l }

type ss_map = m:Map.t var term {
  forall (x:var). (~ (Map.contains m x)) ==> Map.sel m x == tm_unknown
}
val remove_map : m: Pulse.Checker.Prover.Substs.ss_map -> x: Pulse.Syntax.Base.var
  -> FStar.Map.t Pulse.Syntax.Base.var Pulse.Syntax.Base.term
m: Pulse.Checker.Prover.Substs.ss_map -> x: Pulse.Syntax.Base.var
  -> FStar.Map.t Pulse.Syntax.Base.var Pulse.Syntax.Base.term