val freevars (t: term) : Set.set var
let rec freevars (t:term) 
  : Set.set var
  = match t.t with
    | Tm_Emp
    | Tm_VProp
    | Tm_Inames
    | Tm_EmpInames
    | Tm_Unknown -> Set.empty
    | Tm_Star t1 t2 ->
      Set.union (freevars t1) (freevars t2)
    | Tm_ExistsSL _ t1 t2
    | Tm_ForallSL _ t1 t2 ->
      Set.union (freevars t1.binder_ty) (freevars t2)
    | Tm_Pure p -> freevars p
    | Tm_FStar t -> RT.freevars t
val freevars (t: term) : Set.set var
let rec freevars (t: term) : Set.set var =
match t.t with
| Tm_Emp | Tm_VProp | Tm_Inames | Tm_EmpInames | Tm_Unknown -> Set.empty
| Tm_Star t1 t2 -> Set.union (freevars t1) (freevars t2)
| Tm_ExistsSL _ t1 t2 | Tm_ForallSL _ t1 t2 -> Set.union (freevars t1.binder_ty) (freevars t2)
| Tm_Pure p -> freevars p
| Tm_FStar t -> RT.freevars t
Pulse.Syntax.Naming.fsti.checked
Pulse.Syntax.Pure.fst.checked Pulse.Syntax.Base.fsti.checked Pulse.RuntimeUtils.fsti.checked Pulse.Elaborate.Pure.fst.checked Pulse.Common.fst.checked prims.fst.checked FStar.Set.fsti.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 FStar.List.fst.checked
Pulse.Syntax.Naming.fsti
Pulse.Syntax.Base.term Pulse.Syntax.Base.__proj__Mkterm__item__t FStar.Set.empty Pulse.Syntax.Base.var FStar.Set.union Pulse.Syntax.Naming.freevars Pulse.Syntax.Base.universe Pulse.Syntax.Base.binder Pulse.Syntax.Base.__proj__Mkbinder__item__binder_ty Pulse.Syntax.Base.host_term FStar.Reflection.Typing.freevars FStar.Set.set
module Pulse.Syntax.Naming

open FStar.List.Tot
open Pulse.Syntax.Base
open Pulse.Common

module L = FStar.List.Tot

module R = FStar.Reflection
module RTB = FStar.Reflection.Typing.Builtins
module RT = FStar.Reflection.Typing
module RU = Pulse.RuntimeUtils
module U = Pulse.Syntax.Pure
module E = Pulse.Elaborate.Pure

let rec freevars (t:term)
val freevars (t: term) : Set.set var
t: Pulse.Syntax.Base.term -> FStar.Set.set Pulse.Syntax.Base.var