val freevars_close_term_opt' (t: option term) (x: var) (i: index)
    : Lemma
      (ensures
        ((freevars_term_opt (close_term_opt' t x i))
          `Set.equal`
          ((freevars_term_opt t) `set_minus` x))) (decreases t)
let freevars_close_term_opt' (t:option term) (x:var) (i:index)
  : Lemma
    (ensures (freevars_term_opt (close_term_opt' t x i) `Set.equal`
             (freevars_term_opt t `set_minus` x)))
    (decreases t)
  = match t with
    | None -> ()
    | Some t -> freevars_close_term' t x i
val freevars_close_term_opt' (t: option term) (x: var) (i: index)
    : Lemma
      (ensures
        ((freevars_term_opt (close_term_opt' t x i))
          `Set.equal`
          ((freevars_term_opt t) `set_minus` x))) (decreases t)
let freevars_close_term_opt' (t: option term) (x: var) (i: index)
    : Lemma
      (ensures
        ((freevars_term_opt (close_term_opt' t x i))
          `Set.equal`
          ((freevars_term_opt t) `set_minus` x))) (decreases t) =
match t with
| None -> ()
| Some t -> freevars_close_term' t x i
Pulse.Typing.FV.fst.checked
Pulse.Typing.fst.checked Pulse.Syntax.fst.checked Pulse.Soundness.Common.fst.checked Pulse.Elaborate.fsti.checked prims.fst.checked FStar.Set.fsti.checked FStar.Reflection.V2.fst.checked FStar.Reflection.Typing.fsti.checked FStar.Range.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Calc.fsti.checked
Pulse.Typing.FV.fst
FStar.Pervasives.Native.option Pulse.Syntax.Base.term Pulse.Syntax.Base.var Pulse.Syntax.Base.index Pulse.Typing.FV.freevars_close_term' Prims.unit Prims.l_True Prims.squash FStar.Set.equal Pulse.Syntax.Naming.freevars_term_opt Pulse.Syntax.Naming.close_term_opt' Pulse.Typing.FV.set_minus Prims.Nil FStar.Pervasives.pattern
module Pulse.Typing.FV
module RT = FStar.Reflection.Typing
module R = FStar.Reflection.V2
module L = FStar.List.Tot
open FStar.List.Tot
open Pulse.Syntax
open Pulse.Typing
open Pulse.Elaborate
open Pulse.Soundness.Common

let vars_of_rt_env (g:R.env) = Set.intension (fun x -> Some? (RT.lookup_bvar g x))

let freevars_close_term_host_term (t:host_term) (x:var) (i:index)
  : Lemma
    (ensures (freevars (close_term' (tm_fstar t FStar.Range.range_0) x i)
            `Set.equal`
             (freevars (tm_fstar t FStar.Range.range_0) `set_minus` x)))
  = admit()

#push-options "--query_stats --z3rlimit_factor 2"
let rec freevars_close_term' (e:term) (x:var) (i:index)
  : Lemma 
    (ensures freevars (close_term' e x i) `Set.equal`
             (freevars e `set_minus` x))
  = match e.t with
    | Tm_Emp
    | Tm_VProp
    | Tm_Inames
    | Tm_EmpInames
    | Tm_Unknown -> ()

    | Tm_Pure p ->
      freevars_close_term' p x i

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

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

    | Tm_FStar t ->
      freevars_close_term_host_term t x i

let freevars_close_comp (c:comp)
                        (x:var)
                        (i:index)
  : Lemma 
    (ensures freevars_comp (close_comp' c x i) `Set.equal`
             (freevars_comp c `set_minus` x))
    [SMTPat (freevars_comp (close_comp' c x i))]
  = match c with
    | C_Tot t ->
      freevars_close_term' t x i

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

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

let freevars_close_term_opt' (t:option term) (x:var) (i:index)
  : Lemma
    (ensures (freevars_term_opt (close_term_opt' t x i) `Set.equal`
             (freevars_term_opt t `set_minus` x)))
val freevars_close_term_opt' (t: option term) (x: var) (i: index)
    : Lemma
      (ensures
        ((freevars_term_opt (close_term_opt' t x i))
          `Set.equal`
          ((freevars_term_opt t) `set_minus` x))) (decreases t)

    t: FStar.Pervasives.Native.option Pulse.Syntax.Base.term ->
    x: Pulse.Syntax.Base.var ->
    i: Pulse.Syntax.Base.index
  -> FStar.Pervasives.Lemma
      (ensures
        FStar.Set.equal (Pulse.Syntax.Naming.freevars_term_opt (Pulse.Syntax.Naming.close_term_opt' t
                  x
                  i))
          (Pulse.Typing.FV.set_minus (Pulse.Syntax.Naming.freevars_term_opt t) x)) (decreases t)