val 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)
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
val 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)
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
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
Pulse.Syntax.Base.term Pulse.Syntax.Base.var Prims.l_not Prims.b2t FStar.Set.mem Pulse.Syntax.Naming.freevars Pulse.Syntax.Base.index Pulse.Syntax.Base.__proj__Mkterm__item__t Pulse.Syntax.Naming.close_open_inverse' Prims.unit Pulse.Syntax.Base.universe Pulse.Syntax.Base.binder Prims.op_Addition Pulse.Syntax.Base.__proj__Mkbinder__item__binder_ty Pulse.Syntax.Base.host_term FStar.Reflection.Typing.close_open_inverse' Prims.l_True Prims.squash Prims.eq2 Pulse.Syntax.Naming.close_term' Pulse.Syntax.Naming.open_term' 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)
val 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)

    t: Pulse.Syntax.Base.term ->
    x: Pulse.Syntax.Base.var{~(FStar.Set.mem x (Pulse.Syntax.Naming.freevars t))} ->
    i: Pulse.Syntax.Base.index
  -> FStar.Pervasives.Lemma
      (ensures
        Pulse.Syntax.Naming.close_term' (Pulse.Syntax.Naming.open_term' t
              (Pulse.Syntax.Pure.term_of_no_name_var x)
              i)
          x
          i ==
        t) (decreases t)