val close_open_inverse_opt' (t:option term)
                            (x:var { ~(x `Set.mem` freevars_term_opt t) })
                            (i:index)
  : Lemma (ensures close_term_opt' (open_term_opt' t (U.term_of_no_name_var x) i) x i == t)
let close_open_inverse_opt' (t:option term)
                            (x:var { ~(x `Set.mem` freevars_term_opt t) })
                            (i:index)
  : Lemma (ensures close_term_opt' (open_term_opt' t (U.term_of_no_name_var x) i) x i == t)
  = match t with
    | None -> ()
    | Some t -> close_open_inverse' t x i
val close_open_inverse_opt' (t:option term)
                            (x:var { ~(x `Set.mem` freevars_term_opt t) })
                            (i:index)
  : Lemma (ensures close_term_opt' (open_term_opt' t (U.term_of_no_name_var x) i) x i == t)
let close_open_inverse_opt'
      (t: option term)
      (x: var{~(x `Set.mem` (freevars_term_opt t))})
      (i: index)
    : Lemma (ensures close_term_opt' (open_term_opt' t (U.term_of_no_name_var x) i) x i == t) =
match t with
| None -> ()
| Some t -> close_open_inverse' t x i
Pulse.Syntax.Naming.fst.checked
Pulse.Syntax.Pure.fst.checked Pulse.Syntax.Base.fsti.checked Pulse.RuntimeUtils.fsti.checked Pulse.Elaborate.Pure.fst.checked prims.fst.checked FStar.Set.fsti.checked FStar.Reflection.V2.fst.checked FStar.Reflection.Typing.Builtins.fsti.checked FStar.Reflection.Typing.fsti.checked FStar.Reflection.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Pulse.Syntax.Naming.fst
FStar.Pervasives.Native.option Pulse.Syntax.Base.term Pulse.Syntax.Base.var Prims.l_not Prims.b2t FStar.Set.mem Pulse.Syntax.Naming.freevars_term_opt Pulse.Syntax.Base.index Pulse.Syntax.Naming.close_open_inverse' Prims.unit Prims.l_True Prims.squash Prims.eq2 Pulse.Syntax.Naming.close_term_opt' Pulse.Syntax.Naming.open_term_opt' Pulse.Syntax.Pure.term_of_no_name_var Prims.Nil FStar.Pervasives.pattern
module Pulse.Syntax.Naming
module RTB = FStar.Reflection.Typing.Builtins
module RT = FStar.Reflection.Typing
module R = FStar.Reflection
open FStar.List.Tot
module E = Pulse.Elaborate.Pure
open Pulse.Syntax.Base
module U = Pulse.Syntax.Pure
module R2 = FStar.Reflection.V2
module RU = Pulse.RuntimeUtils
let r_subst_of_rt_subst_elt (x:subst_elt)
  : FStar.Reflection.V2.subst_elt
  = match x with
    | DT i t -> R2.DT i (E.elab_term t)
    | NT x t -> R2.NT (RT.var_as_namedv x) (E.elab_term t) 
    | ND x i -> R2.NM (RT.var_as_namedv x) i

let subst_host_term' (t:host_term) (ss:subst) =
  R2.subst_term (L.map r_subst_of_rt_subst_elt ss) t

let subst_host_term (t:host_term) (ss:subst) =
  open_or_close_host_term t ss;  
  let res0 = subst_host_term' t ss in
  assume (res0 == RT.subst_term t (rt_subst ss));
  res0

// let subst_host_term (t:host_term) (ss:subst) =
//   open_or_close_host_term t ss;  
//   RT.subst_term t (rt_subst ss)

let rec close_open_inverse' (t:term) 
                            (x:var { ~(x `Set.mem` freevars t) } )
                            (i:index)
  : Lemma (ensures close_term' (open_term' t (U.term_of_no_name_var x) i) x i == t)
          (decreases t)
  = match t.t with
    | Tm_Emp
    | Tm_VProp
    | Tm_Inames 
    | Tm_EmpInames
    | Tm_Unknown -> ()
    
    | Tm_Pure p ->
      close_open_inverse' p x i

    | Tm_Star l r ->
      close_open_inverse' l x i;
      close_open_inverse' r x i

    | Tm_ExistsSL _ t b
    | Tm_ForallSL _ t b ->
      close_open_inverse' t.binder_ty x i;    
      close_open_inverse' b x (i + 1)

    | Tm_FStar t ->
      RT.close_open_inverse' i t x

let close_open_inverse_comp' (c:comp)
                             (x:var { ~(x `Set.mem` freevars_comp c) } )
                             (i:index)
  : Lemma (ensures close_comp' (open_comp' c (U.term_of_no_name_var x) i) x i == c)
  = match c with
    | C_Tot t ->
      close_open_inverse' t x i

    | C_ST s ->
      close_open_inverse' s.res x i;
      close_open_inverse' s.pre x i;      
      close_open_inverse' s.post x (i + 1)

    | C_STAtomic n s
    | C_STGhost n s ->    
      close_open_inverse' n x i;    
      close_open_inverse' s.res x i;
      close_open_inverse' s.pre x i;      
      close_open_inverse' s.post x (i + 1)

let close_open_inverse_opt' (t:option term)
                            (x:var { ~(x `Set.mem` freevars_term_opt t) })
                            (i:index)
val close_open_inverse_opt' (t:option term)
                            (x:var { ~(x `Set.mem` freevars_term_opt t) })
                            (i:index)
  : Lemma (ensures close_term_opt' (open_term_opt' t (U.term_of_no_name_var x) i) x i == t)

    t: FStar.Pervasives.Native.option Pulse.Syntax.Base.term ->
    x: Pulse.Syntax.Base.var{~(FStar.Set.mem x (Pulse.Syntax.Naming.freevars_term_opt t))} ->
    i: Pulse.Syntax.Base.index
  -> FStar.Pervasives.Lemma
    (ensures
      Pulse.Syntax.Naming.close_term_opt' (Pulse.Syntax.Naming.open_term_opt' t
            (Pulse.Syntax.Pure.term_of_no_name_var x)
            i)
        x
        i ==
      t)