val freevars_close_proof_hint' (ht: proof_hint_type) (x: var) (i: index)
    : Lemma
    (ensures
      ((freevars_proof_hint (close_proof_hint' ht x i))
        `Set.equal`
        ((freevars_proof_hint ht) `set_minus` x)))
let freevars_close_proof_hint' (ht:proof_hint_type) (x:var) (i:index)
  : Lemma
    (ensures (freevars_proof_hint (close_proof_hint' ht x i) `Set.equal`
             (freevars_proof_hint ht `set_minus` x)))
  = match ht with
    | ASSERT { p }
    | FOLD { p }
    | UNFOLD { p } ->
      freevars_close_term' p x i
    | RENAME { pairs; goal } ->
      freevars_close_term_pairs' pairs x i;
      freevars_close_term_opt' goal x i
    | REWRITE { t1; t2 } ->
      freevars_close_term' t1 x i;
      freevars_close_term' t2 x i
val freevars_close_proof_hint' (ht: proof_hint_type) (x: var) (i: index)
    : Lemma
    (ensures
      ((freevars_proof_hint (close_proof_hint' ht x i))
        `Set.equal`
        ((freevars_proof_hint ht) `set_minus` x)))
let freevars_close_proof_hint' (ht: proof_hint_type) (x: var) (i: index)
    : Lemma
    (ensures
      ((freevars_proof_hint (close_proof_hint' ht x i))
        `Set.equal`
        ((freevars_proof_hint ht) `set_minus` x))) =
match ht with
| ASSERT { p = p } | FOLD { p = p } | UNFOLD { p = p } -> freevars_close_term' p x i
| RENAME { pairs = pairs ; goal = goal } ->
  freevars_close_term_pairs' pairs x i;
  freevars_close_term_opt' goal x i
| REWRITE { t1 = t1 ; t2 = t2 } ->
  freevars_close_term' t1 x i;
  freevars_close_term' t2 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
Pulse.Syntax.Base.proof_hint_type Pulse.Syntax.Base.var Pulse.Syntax.Base.index Pulse.Syntax.Base.vprop Pulse.Typing.FV.freevars_close_term' FStar.Pervasives.Native.option Prims.list Prims.string FStar.Pervasives.Native.tuple2 Pulse.Syntax.Base.term Pulse.Typing.FV.freevars_close_term_opt' Prims.unit Pulse.Typing.FV.freevars_close_term_pairs' Prims.l_True Prims.squash FStar.Set.equal Pulse.Syntax.Naming.freevars_proof_hint Pulse.Syntax.Naming.close_proof_hint' 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)))
    (decreases t)
  = match t with
    | None -> ()
    | Some t -> freevars_close_term' t x i

let rec freevars_close_term_list' (t:list term) (x:var) (i:index)
  : Lemma
    (ensures (freevars_list (close_term_list' t x i) `Set.equal`
             (freevars_list t `set_minus` x)))
    (decreases t)
  = match t with
    | [] -> ()
    | hd::tl ->
      freevars_close_term' hd x i;
      freevars_close_term_list' tl x i

let rec freevars_close_term_pairs' (t:list (term & term)) (x:var) (i:index)
  : Lemma
    (ensures (freevars_pairs (close_term_pairs' t x i) `Set.equal`
             (freevars_pairs t `set_minus` x)))
    (decreases t)
  = match t with
    | [] -> ()
    | (u, v)::tl ->
      freevars_close_term' u x i;
      freevars_close_term' v x i;
      freevars_close_term_pairs' tl x i

let freevars_close_proof_hint' (ht:proof_hint_type) (x:var) (i:index)
  : Lemma
    (ensures (freevars_proof_hint (close_proof_hint' ht x i) `Set.equal`
val freevars_close_proof_hint' (ht: proof_hint_type) (x: var) (i: index)
    : Lemma
    (ensures
      ((freevars_proof_hint (close_proof_hint' ht x i))
        `Set.equal`
        ((freevars_proof_hint ht) `set_minus` x)))
ht: Pulse.Syntax.Base.proof_hint_type -> x: Pulse.Syntax.Base.var -> i: Pulse.Syntax.Base.index
  -> FStar.Pervasives.Lemma
    (ensures
      FStar.Set.equal (Pulse.Syntax.Naming.freevars_proof_hint (Pulse.Syntax.Naming.close_proof_hint'
                ht
                x
                i))
        (Pulse.Typing.FV.set_minus (Pulse.Syntax.Naming.freevars_proof_hint ht) x))