val is_dom_push (l: ss_dom) (m: ss_map{is_dom l m}) (x: var{~(Map.contains m x)}) (t: term)
    : Lemma (is_dom (x :: l) (Map.upd m x t))
let is_dom_push
  (l:ss_dom)
  (m:ss_map { is_dom l m })
  (x:var { ~ (Map.contains m x ) })
  (t:term)
  : Lemma (is_dom (x::l) (Map.upd m x t)) =

  assert (Map.equal (remove_map (Map.upd m x t) x) m)
val is_dom_push (l: ss_dom) (m: ss_map{is_dom l m}) (x: var{~(Map.contains m x)}) (t: term)
    : Lemma (is_dom (x :: l) (Map.upd m x t))
let is_dom_push (l: ss_dom) (m: ss_map{is_dom l m}) (x: var{~(Map.contains m x)}) (t: term)
    : Lemma (is_dom (x :: l) (Map.upd m x t)) =
assert (Map.equal (remove_map (Map.upd m x t) x) m)
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_dom Pulse.Checker.Prover.Substs.ss_map Pulse.Checker.Prover.Substs.is_dom Pulse.Syntax.Base.var Prims.l_not Prims.b2t FStar.Map.contains Pulse.Syntax.Base.term Prims._assert FStar.Map.equal Pulse.Checker.Prover.Substs.remove_map FStar.Map.upd Prims.unit Prims.l_True Prims.squash Prims.Cons Prims.Nil FStar.Pervasives.pattern
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
}

let remove_map (m:ss_map) (x:var) =
  Map.restrict (Set.complement (Set.singleton x)) (Map.upd m x tm_unknown)

let rec is_dom (l:ss_dom) (m:ss_map) : Type0 =
  match l with
  | [] -> Set.equal (Map.domain m) Set.empty
  | x::tl ->
    Map.contains m x /\ is_dom tl (remove_map m x)

let rec is_dom_mem (l:ss_dom) (m:ss_map)
  : Lemma
      (requires is_dom l m)
      (ensures forall (x:var).{:pattern L.memP x l \/ Map.contains m x}
                              L.memP x l <==> Map.contains m x)
      [SMTPat (is_dom l m)] =
  match l with
  | [] -> ()
  | y::tl -> is_dom_mem tl (remove_map m y)

noeq
type ss_t = {
  l : ss_dom;
  m : m:ss_map { is_dom l m }
}

let as_map (ss:ss_t) = ss.m

let empty = { l = []; m = Map.const_on Set.empty tm_unknown }

let is_dom_push
  (l:ss_dom)
  (m:ss_map { is_dom l m })
  (x:var { ~ (Map.contains m x ) })
  (t:term)
  : Lemma (is_dom (x::l) (Map.upd m x t)) =
val is_dom_push (l: ss_dom) (m: ss_map{is_dom l m}) (x: var{~(Map.contains m x)}) (t: term)
    : Lemma (is_dom (x :: l) (Map.upd m x t))

    l: Pulse.Checker.Prover.Substs.ss_dom ->
    m: Pulse.Checker.Prover.Substs.ss_map{Pulse.Checker.Prover.Substs.is_dom l m} ->
    x: Pulse.Syntax.Base.var{~(FStar.Map.contains m x)} ->
    t: Pulse.Syntax.Base.term
  -> FStar.Pervasives.Lemma
    (ensures Pulse.Checker.Prover.Substs.is_dom (x :: l) (FStar.Map.upd m x t))