val freevars_ty (t: src_ty) : Set.set var
val freevars_ty (t: src_ty) : Set.set var
let rec freevars (e:src_exp) 
  : FStar.Set.set var
  = match e with
    | EVar v -> Set.singleton v
    | EBool _
    | EBVar _ -> Set.empty
    | EIf b e1 e2 -> Set.union (freevars b) (Set.union (freevars e1) (freevars e2))
    | ELam t e -> Set.union (freevars_ty t) (freevars e)
    | EApp e1 e2 -> Set.union (freevars e1) (freevars e2)
and freevars_ty (t:src_ty)
  : Set.set var
  = match t with
    | TBool -> Set.empty
    | TArrow t1 t2 -> freevars_ty t1 `Set.union` freevars_ty t2
    | TRefineBool e -> freevars e
module BoolRefinement
module T = FStar.Tactics.V2
module R = FStar.Reflection.V2
module L = FStar.List.Tot
open FStar.List.Tot
#push-options "--z3cliopt 'smt.qi.eager_threshold=100' --z3cliopt 'smt.arith.nl=false'"

let var = nat
let index = nat

let tun = R.pack_ln R.Tv_Unknown

type src_exp =
  | EBVar : index -> src_exp
  | EVar  : var -> src_exp
  | EBool : bool -> src_exp
  | EIf   : src_exp -> src_exp -> src_exp -> src_exp
  | ELam  : src_ty -> src_exp -> src_exp
  | EApp  : src_exp -> src_exp -> src_exp

and src_ty =
  | TBool : src_ty
  | TRefineBool : src_exp -> src_ty
  | TArrow : src_ty -> src_ty -> src_ty

let rec size (e:src_exp)
  : nat
  = match e with
    | EBool _
    | EBVar _ 
    | EVar _ -> 1
    | EIf b e1 e2 -> size b + size e1 + size e2 + 1
    | ELam _ e -> 1 + size e
    | EApp e1 e2 -> 1 + size e1 + size e2
/
prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Stubs.Tactics.V2.Builtins.fsti.checked FStar.Squash.fsti.checked FStar.Set.fsti.checked FStar.Reflection.V2.fst.checked FStar.Reflection.Typing.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
BoolRefinement.fst
t: BoolRefinement.src_ty -> FStar.Set.set BoolRefinement.var
BoolRefinement.src_ty FStar.Set.empty BoolRefinement.var FStar.Set.union BoolRefinement.freevars_ty BoolRefinement.src_exp BoolRefinement.freevars FStar.Set.set
let rec freevars_ty (t: src_ty) : Set.set var =
  
match t with
| TBool -> Set.empty
| TArrow t1 t2 -> (freevars_ty t1) `Set.union` (freevars_ty t2)
| TRefineBool e -> freevars e